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  2527  reubida  2715  rmobida  2721  mpteq12f  4169  reuhypd  4568  funbrfv2b  5690  dffn5im  5691  eqfnfv2  5745  fndmin  5754  fniniseg  5767  rexsupp  5771  fmptco  5813  dff13  5909  riotabidva  5989  mpoeq123dva  6082  mpoeq3dva  6085  mpoxopovel  6407  qliftfun  6786  erovlem  6796  xpcomco  7010  pw2f1odclem  7020  elfi2  7171  ctssdccl  7310  ltexpi  7557  dfplpq2  7574  axprecex  8100  zrevaddcl  9530  qrevaddcl  9878  icoshft  10225  fznn  10324  pfxeq  11281  pfxsuffeqwrdeq  11283  pfxsuff1eqwrdeq  11284  shftdm  11400  2shfti  11409  sumeq2  11937  fsum3  11966  fsum2dlemstep  12013  prodeq2  12136  fprodseq  12162  bitsmod  12535  bitscmp  12537  gcdaddm  12573  grpidpropdg  13475  ismgmid  13478  gsumpropd2  13494  mhmpropd  13567  issubm2  13574  eqgid  13831  eqgabl  13935  rngpropd  13987  iscrng2  14047  ringpropd  14070  crngpropd  14071  crngunit  14144  dvdsrpropdg  14180  issubrg3  14280  lsslss  14414  lsspropdg  14464  znleval  14686  bastop2  14827  restopn2  14926  iscnp3  14946  lmbr2  14957  txlm  15022  ismet2  15097  xblpnfps  15141  xblpnf  15142  blininf  15167  blres  15177  elmopn2  15192  neibl  15234  metrest  15249  metcnp3  15254  metcnp  15255  metcnp2  15256  metcn  15257  txmetcn  15262  cnbl0  15277  cnblcld  15278  bl2ioo  15293  elcncf2  15317  cncfmet  15335  cnlimc  15415  lgsquadlem1  15825  lgsquadlem2  15826  2lgslem1a  15836  upgriswlkdc  16230  isclwwlknx  16286  clwwlkn1  16288  clwwlkn2  16291  eupth2lemsfi  16348