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  2537  reubida  2726  rmobida  2732  mpteq12f  4190  reuhypd  4592  funbrfv2b  5721  dffn5im  5722  eqfnfv2  5776  fndmin  5785  fniniseg  5798  fmptco  5843  dff13  5941  riotabidva  6021  mpoeq123dva  6114  mpoeq3dva  6117  suppssrst  6461  suppssrgst  6462  mpoxopovel  6472  qliftfun  6851  erovlem  6861  mapsnend  7052  xpcomco  7077  pw2f1odclem  7087  elfi2  7259  ctssdccl  7402  ltexpi  7652  dfplpq2  7669  axprecex  8195  zrevaddcl  9628  qrevaddcl  9976  icoshft  10323  fznn  10423  sseqn  11203  pfxeq  11388  pfxsuffeqwrdeq  11390  pfxsuff1eqwrdeq  11391  shftdm  11507  2shfti  11516  sumeq2  12044  fsum3  12073  fsum2dlemstep  12120  prodeq2  12243  fprodseq  12269  bitsmod  12642  bitscmp  12644  gcdaddm  12680  grpidpropdg  13587  ismgmid  13590  gsumpropd2  13606  mhmpropd  13679  issubm2  13686  eqgid  13943  eqgabl  14047  rngpropd  14099  iscrng2  14159  ringpropd  14182  crngpropd  14183  crngunit  14256  dvdsrpropdg  14292  issubrg3  14392  lsslss  14529  lsspropdg  14579  znleval  14801  bastop2  14949  restopn2  15048  iscnp3  15068  lmbr2  15079  txlm  15144  ismet2  15219  xblpnfps  15263  xblpnf  15264  blininf  15289  blres  15299  elmopn2  15314  neibl  15356  metrest  15371  metcnp3  15376  metcnp  15377  metcnp2  15378  metcn  15379  txmetcn  15384  cnbl0  15399  cnblcld  15400  bl2ioo  15415  elcncf2  15439  cncfmet  15457  cnlimc  15537  lgsquadlem1  15950  lgsquadlem2  15951  2lgslem1a  15961  upgriswlkdc  16355  isclwwlknx  16411  clwwlkn1  16413  clwwlkn2  16416  eupth2lemsfi  16473