Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  imdistanda Unicode version

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
StepHypRef Expression
1 imdistanda.1 . . 3
21ex 434 . 2
32imdistand 692 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator