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  2492  reubida  2679  rmobida  2684  mpteq12f  4113  reuhypd  4506  funbrfv2b  5605  dffn5im  5606  eqfnfv2  5660  fndmin  5669  fniniseg  5682  rexsupp  5686  fmptco  5728  dff13  5815  riotabidva  5894  mpoeq123dva  5983  mpoeq3dva  5986  mpoxopovel  6299  qliftfun  6676  erovlem  6686  xpcomco  6885  pw2f1odclem  6895  elfi2  7038  ctssdccl  7177  ltexpi  7404  dfplpq2  7421  axprecex  7947  zrevaddcl  9376  qrevaddcl  9718  icoshft  10065  fznn  10164  shftdm  10987  2shfti  10996  sumeq2  11524  fsum3  11552  fsum2dlemstep  11599  prodeq2  11722  fprodseq  11748  gcdaddm  12151  grpidpropdg  13017  ismgmid  13020  gsumpropd2  13036  mhmpropd  13098  issubm2  13105  eqgid  13356  eqgabl  13460  rngpropd  13511  iscrng2  13571  ringpropd  13594  crngpropd  13595  crngunit  13667  dvdsrpropdg  13703  issubrg3  13803  lsslss  13937  lsspropdg  13987  znleval  14209  bastop2  14320  restopn2  14419  iscnp3  14439  lmbr2  14450  txlm  14515  ismet2  14590  xblpnfps  14634  xblpnf  14635  blininf  14660  blres  14670  elmopn2  14685  neibl  14727  metrest  14742  metcnp3  14747  metcnp  14748  metcnp2  14749  metcn  14750  txmetcn  14755  cnbl0  14770  cnblcld  14771  bl2ioo  14786  elcncf2  14810  cncfmet  14828  cnlimc  14908  lgsquadlem1  15318  lgsquadlem2  15319  2lgslem1a  15329