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  2525  reubida  2713  rmobida  2719  mpteq12f  4167  reuhypd  4566  funbrfv2b  5686  dffn5im  5687  eqfnfv2  5741  fndmin  5750  fniniseg  5763  rexsupp  5767  fmptco  5809  dff13  5904  riotabidva  5984  mpoeq123dva  6077  mpoeq3dva  6080  mpoxopovel  6402  qliftfun  6781  erovlem  6791  xpcomco  7005  pw2f1odclem  7015  elfi2  7162  ctssdccl  7301  ltexpi  7547  dfplpq2  7564  axprecex  8090  zrevaddcl  9520  qrevaddcl  9868  icoshft  10215  fznn  10314  pfxeq  11267  pfxsuffeqwrdeq  11269  pfxsuff1eqwrdeq  11270  shftdm  11373  2shfti  11382  sumeq2  11910  fsum3  11938  fsum2dlemstep  11985  prodeq2  12108  fprodseq  12134  bitsmod  12507  bitscmp  12509  gcdaddm  12545  grpidpropdg  13447  ismgmid  13450  gsumpropd2  13466  mhmpropd  13539  issubm2  13546  eqgid  13803  eqgabl  13907  rngpropd  13958  iscrng2  14018  ringpropd  14041  crngpropd  14042  crngunit  14115  dvdsrpropdg  14151  issubrg3  14251  lsslss  14385  lsspropdg  14435  znleval  14657  bastop2  14798  restopn2  14897  iscnp3  14917  lmbr2  14928  txlm  14993  ismet2  15068  xblpnfps  15112  xblpnf  15113  blininf  15138  blres  15148  elmopn2  15163  neibl  15205  metrest  15220  metcnp3  15225  metcnp  15226  metcnp2  15227  metcn  15228  txmetcn  15233  cnbl0  15248  cnblcld  15249  bl2ioo  15264  elcncf2  15288  cncfmet  15306  cnlimc  15386  lgsquadlem1  15796  lgsquadlem2  15797  2lgslem1a  15807  upgriswlkdc  16157  isclwwlknx  16211  clwwlkn1  16213  clwwlkn2  16216