Theorem imdistanda 693

Description: Distribution of implication with conjunction (deduction version with conjoined antecedent). (Contributed by Jeff Madsen, 19-Jun-2011.)

Hypothesis

Ref	Expression
imdistanda.1

Assertion

Ref	Expression
imdistanda

Proof of Theorem imdistanda

Step	Hyp	Ref	Expression
1		imdistanda.1	. . 3
2	1	ex 434	. 2
3	2	imdistand 692	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  cfub  8650  cflm  8651  fzind  10987  uzss  11130  cau3lem  13187  supcvg  13667  eulerthlem2  14312  pgpfac1lem3  17128  iscnp4  19764  cncls2  19774  cncls  19775  cnntr  19776  1stcelcls  19962  cnpflf  20502  fclsnei  20520  cnpfcf  20542  alexsublem  20544  iscau4  21718  caussi  21736  equivcfil  21738  ismbf3d  22061  i1fmullem  22101  abelth  22836  ocsh  26201  fpwrelmap  27556  locfinreflem  27843  isdrngo3  30362  keridl  30429  pmapjat1  35577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371