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  2482  reubida  2669  rmobida  2674  mpteq12f  4095  reuhypd  4483  funbrfv2b  5573  dffn5im  5574  eqfnfv2  5627  fndmin  5636  fniniseg  5649  rexsupp  5653  fmptco  5695  dff13  5782  riotabidva  5860  mpoeq123dva  5949  mpoeq3dva  5952  mpoxopovel  6255  qliftfun  6630  erovlem  6640  xpcomco  6839  elfi2  6984  ctssdccl  7123  ltexpi  7349  dfplpq2  7366  axprecex  7892  zrevaddcl  9316  qrevaddcl  9657  icoshft  10003  fznn  10102  shftdm  10844  2shfti  10853  sumeq2  11380  fsum3  11408  fsum2dlemstep  11455  prodeq2  11578  fprodseq  11604  gcdaddm  11998  grpidpropdg  12811  ismgmid  12814  mhmpropd  12876  issubm2  12883  eqgid  13115  iscrng2  13252  ringpropd  13275  crngpropd  13276  crngunit  13343  dvdsrpropdg  13379  issubrg3  13431  lsslss  13534  lsspropdg  13584  bastop2  13824  restopn2  13923  iscnp3  13943  lmbr2  13954  txlm  14019  ismet2  14094  xblpnfps  14138  xblpnf  14139  blininf  14164  blres  14174  elmopn2  14189  neibl  14231  metrest  14246  metcnp3  14251  metcnp  14252  metcnp2  14253  metcn  14254  txmetcn  14259  cnbl0  14274  cnblcld  14275  bl2ioo  14282  elcncf2  14301  cncfmet  14319  cnlimc  14381