Theorem pm5.32da 449

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 114	. 2 |- ( ph -> ( ps -> ( ch <-> th ) ) )
3	2	pm5.32d 447	1 |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  rexbida  2465  reubida  2651  rmobida  2656  mpteq12f  4069  reuhypd  4456  funbrfv2b  5541  dffn5im  5542  eqfnfv2  5594  fndmin  5603  fniniseg  5616  rexsupp  5620  fmptco  5662  dff13  5747  riotabidva  5825  mpoeq123dva  5914  mpoeq3dva  5917  mpoxopovel  6220  qliftfun  6595  erovlem  6605  xpcomco  6804  elfi2  6949  ctssdccl  7088  ltexpi  7299  dfplpq2  7316  axprecex  7842  zrevaddcl  9262  qrevaddcl  9603  icoshft  9947  fznn  10045  shftdm  10786  2shfti  10795  sumeq2  11322  fsum3  11350  fsum2dlemstep  11397  prodeq2  11520  fprodseq  11546  gcdaddm  11939  grpidpropdg  12628  ismgmid  12631  mhmpropd  12689  bastop2  12878  restopn2  12977  iscnp3  12997  lmbr2  13008  txlm  13073  ismet2  13148  xblpnfps  13192  xblpnf  13193  blininf  13218  blres  13228  elmopn2  13243  neibl  13285  metrest  13300  metcnp3  13305  metcnp  13306  metcnp2  13307  metcn  13308  txmetcn  13313  cnbl0  13328  cnblcld  13329  bl2ioo  13336  elcncf2  13355  cncfmet  13373  cnlimc  13435