Theorem pm5.32da 452

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 9-Dec-2006.)

Hypothesis

Ref	Expression
pm5.32da.1	|- ( ( ph /\ ps ) -> ( ch <-> th ) )

Assertion

Ref	Expression
pm5.32da	|- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )

Proof of Theorem pm5.32da

Step	Hyp	Ref	Expression
1		pm5.32da.1	. . 3 |- ( ( ph /\ ps ) -> ( ch <-> th ) )
2	1	ex 115	. 2 |- ( ph -> ( ps -> ( ch <-> th ) ) )
3	2	pm5.32d 450	1 |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexbida  2528  reubida  2716  rmobida  2722  mpteq12f  4174  reuhypd  4574  funbrfv2b  5699  dffn5im  5700  eqfnfv2  5754  fndmin  5763  fniniseg  5776  fmptco  5821  dff13  5919  riotabidva  5999  mpoeq123dva  6092  mpoeq3dva  6095  suppssrst  6439  suppssrgst  6440  mpoxopovel  6450  qliftfun  6829  erovlem  6839  xpcomco  7053  pw2f1odclem  7063  elfi2  7214  ctssdccl  7353  ltexpi  7600  dfplpq2  7617  axprecex  8143  zrevaddcl  9574  qrevaddcl  9922  icoshft  10269  fznn  10369  pfxeq  11326  pfxsuffeqwrdeq  11328  pfxsuff1eqwrdeq  11329  shftdm  11445  2shfti  11454  sumeq2  11982  fsum3  12011  fsum2dlemstep  12058  prodeq2  12181  fprodseq  12207  bitsmod  12580  bitscmp  12582  gcdaddm  12618  grpidpropdg  13520  ismgmid  13523  gsumpropd2  13539  mhmpropd  13612  issubm2  13619  eqgid  13876  eqgabl  13980  rngpropd  14032  iscrng2  14092  ringpropd  14115  crngpropd  14116  crngunit  14189  dvdsrpropdg  14225  issubrg3  14325  lsslss  14460  lsspropdg  14510  znleval  14732  bastop2  14878  restopn2  14977  iscnp3  14997  lmbr2  15008  txlm  15073  ismet2  15148  xblpnfps  15192  xblpnf  15193  blininf  15218  blres  15228  elmopn2  15243  neibl  15285  metrest  15300  metcnp3  15305  metcnp  15306  metcnp2  15307  metcn  15308  txmetcn  15313  cnbl0  15328  cnblcld  15329  bl2ioo  15344  elcncf2  15368  cncfmet  15386  cnlimc  15466  lgsquadlem1  15879  lgsquadlem2  15880  2lgslem1a  15890  upgriswlkdc  16284  isclwwlknx  16340  clwwlkn1  16342  clwwlkn2  16345  eupth2lemsfi  16402