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  2659  rmobida  2664  mpteq12f  4085  reuhypd  4473  funbrfv2b  5562  dffn5im  5563  eqfnfv2  5616  fndmin  5625  fniniseg  5638  rexsupp  5642  fmptco  5684  dff13  5771  riotabidva  5849  mpoeq123dva  5938  mpoeq3dva  5941  mpoxopovel  6244  qliftfun  6619  erovlem  6629  xpcomco  6828  elfi2  6973  ctssdccl  7112  ltexpi  7338  dfplpq2  7355  axprecex  7881  zrevaddcl  9305  qrevaddcl  9646  icoshft  9992  fznn  10091  shftdm  10833  2shfti  10842  sumeq2  11369  fsum3  11397  fsum2dlemstep  11444  prodeq2  11567  fprodseq  11593  gcdaddm  11987  grpidpropdg  12798  ismgmid  12801  mhmpropd  12862  issubm2  12869  eqgid  13090  iscrng2  13203  ringpropd  13222  crngpropd  13223  crngunit  13285  dvdsrpropdg  13321  issubrg3  13373  lsslss  13473  bastop2  13623  restopn2  13722  iscnp3  13742  lmbr2  13753  txlm  13818  ismet2  13893  xblpnfps  13937  xblpnf  13938  blininf  13963  blres  13973  elmopn2  13988  neibl  14030  metrest  14045  metcnp3  14050  metcnp  14051  metcnp2  14052  metcn  14053  txmetcn  14058  cnbl0  14073  cnblcld  14074  bl2ioo  14081  elcncf2  14100  cncfmet  14118  cnlimc  14180