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  2500  reubida  2687  rmobida  2692  mpteq12f  4123  reuhypd  4517  funbrfv2b  5622  dffn5im  5623  eqfnfv2  5677  fndmin  5686  fniniseg  5699  rexsupp  5703  fmptco  5745  dff13  5836  riotabidva  5915  mpoeq123dva  6005  mpoeq3dva  6008  mpoxopovel  6326  qliftfun  6703  erovlem  6713  xpcomco  6920  pw2f1odclem  6930  elfi2  7073  ctssdccl  7212  ltexpi  7449  dfplpq2  7466  axprecex  7992  zrevaddcl  9422  qrevaddcl  9764  icoshft  10111  fznn  10210  shftdm  11104  2shfti  11113  sumeq2  11641  fsum3  11669  fsum2dlemstep  11716  prodeq2  11839  fprodseq  11865  bitsmod  12238  bitscmp  12240  gcdaddm  12276  grpidpropdg  13177  ismgmid  13180  gsumpropd2  13196  mhmpropd  13269  issubm2  13276  eqgid  13533  eqgabl  13637  rngpropd  13688  iscrng2  13748  ringpropd  13771  crngpropd  13772  crngunit  13844  dvdsrpropdg  13880  issubrg3  13980  lsslss  14114  lsspropdg  14164  znleval  14386  bastop2  14527  restopn2  14626  iscnp3  14646  lmbr2  14657  txlm  14722  ismet2  14797  xblpnfps  14841  xblpnf  14842  blininf  14867  blres  14877  elmopn2  14892  neibl  14934  metrest  14949  metcnp3  14954  metcnp  14955  metcnp2  14956  metcn  14957  txmetcn  14962  cnbl0  14977  cnblcld  14978  bl2ioo  14993  elcncf2  15017  cncfmet  15035  cnlimc  15115  lgsquadlem1  15525  lgsquadlem2  15526  2lgslem1a  15536