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  2472  reubida  2658  rmobida  2663  mpteq12f  4081  reuhypd  4469  funbrfv2b  5557  dffn5im  5558  eqfnfv2  5611  fndmin  5620  fniniseg  5633  rexsupp  5637  fmptco  5679  dff13  5764  riotabidva  5842  mpoeq123dva  5931  mpoeq3dva  5934  mpoxopovel  6237  qliftfun  6612  erovlem  6622  xpcomco  6821  elfi2  6966  ctssdccl  7105  ltexpi  7331  dfplpq2  7348  axprecex  7874  zrevaddcl  9297  qrevaddcl  9638  icoshft  9984  fznn  10082  shftdm  10822  2shfti  10831  sumeq2  11358  fsum3  11386  fsum2dlemstep  11433  prodeq2  11556  fprodseq  11582  gcdaddm  11975  grpidpropdg  12723  ismgmid  12726  mhmpropd  12785  issubm2  12792  iscrng2  13098  ringpropd  13117  crngpropd  13118  crngunit  13179  dvdsrpropdg  13215  bastop2  13366  restopn2  13465  iscnp3  13485  lmbr2  13496  txlm  13561  ismet2  13636  xblpnfps  13680  xblpnf  13681  blininf  13706  blres  13716  elmopn2  13731  neibl  13773  metrest  13788  metcnp3  13793  metcnp  13794  metcnp2  13795  metcn  13796  txmetcn  13801  cnbl0  13816  cnblcld  13817  bl2ioo  13824  elcncf2  13843  cncfmet  13861  cnlimc  13923