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  2470  reubida  2656  rmobida  2661  mpteq12f  4078  reuhypd  4465  funbrfv2b  5552  dffn5im  5553  eqfnfv2  5606  fndmin  5615  fniniseg  5628  rexsupp  5632  fmptco  5674  dff13  5759  riotabidva  5837  mpoeq123dva  5926  mpoeq3dva  5929  mpoxopovel  6232  qliftfun  6607  erovlem  6617  xpcomco  6816  elfi2  6961  ctssdccl  7100  ltexpi  7311  dfplpq2  7328  axprecex  7854  zrevaddcl  9274  qrevaddcl  9615  icoshft  9959  fznn  10057  shftdm  10797  2shfti  10806  sumeq2  11333  fsum3  11361  fsum2dlemstep  11408  prodeq2  11531  fprodseq  11557  gcdaddm  11950  grpidpropdg  12657  ismgmid  12660  mhmpropd  12718  iscrng2  12993  ringpropd  13011  crngpropd  13012  bastop2  13153  restopn2  13252  iscnp3  13272  lmbr2  13283  txlm  13348  ismet2  13423  xblpnfps  13467  xblpnf  13468  blininf  13493  blres  13503  elmopn2  13518  neibl  13560  metrest  13575  metcnp3  13580  metcnp  13581  metcnp2  13582  metcn  13583  txmetcn  13588  cnbl0  13603  cnblcld  13604  bl2ioo  13611  elcncf2  13630  cncfmet  13648  cnlimc  13710