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  4164  reuhypd  4562  funbrfv2b  5680  dffn5im  5681  eqfnfv2  5735  fndmin  5744  fniniseg  5757  rexsupp  5761  fmptco  5803  dff13  5898  riotabidva  5978  mpoeq123dva  6071  mpoeq3dva  6074  mpoxopovel  6393  qliftfun  6772  erovlem  6782  xpcomco  6993  pw2f1odclem  7003  elfi2  7150  ctssdccl  7289  ltexpi  7535  dfplpq2  7552  axprecex  8078  zrevaddcl  9508  qrevaddcl  9851  icoshft  10198  fznn  10297  pfxeq  11243  pfxsuffeqwrdeq  11245  pfxsuff1eqwrdeq  11246  shftdm  11348  2shfti  11357  sumeq2  11885  fsum3  11913  fsum2dlemstep  11960  prodeq2  12083  fprodseq  12109  bitsmod  12482  bitscmp  12484  gcdaddm  12520  grpidpropdg  13422  ismgmid  13425  gsumpropd2  13441  mhmpropd  13514  issubm2  13521  eqgid  13778  eqgabl  13882  rngpropd  13933  iscrng2  13993  ringpropd  14016  crngpropd  14017  crngunit  14090  dvdsrpropdg  14126  issubrg3  14226  lsslss  14360  lsspropdg  14410  znleval  14632  bastop2  14773  restopn2  14872  iscnp3  14892  lmbr2  14903  txlm  14968  ismet2  15043  xblpnfps  15087  xblpnf  15088  blininf  15113  blres  15123  elmopn2  15138  neibl  15180  metrest  15195  metcnp3  15200  metcnp  15201  metcnp2  15202  metcn  15203  txmetcn  15208  cnbl0  15223  cnblcld  15224  bl2ioo  15239  elcncf2  15263  cncfmet  15281  cnlimc  15361  lgsquadlem1  15771  lgsquadlem2  15772  2lgslem1a  15782  upgriswlkdc  16101