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  2539  reubida  2728  rmobida  2734  mpteq12f  4195  reuhypd  4597  funbrfv2b  5726  dffn5im  5727  eqfnfv2  5781  fndmin  5790  fniniseg  5803  fmptco  5848  dff13  5947  riotabidva  6029  mpoeq123dva  6122  mpoeq3dva  6125  suppssrst  6474  suppssrgst  6475  mpoxopovel  6485  qliftfun  6864  erovlem  6874  mapsnend  7065  xpcomco  7090  pw2f1odclem  7100  elfi2  7272  ctssdccl  7415  ltexpi  7668  dfplpq2  7685  axprecex  8211  zrevaddcl  9645  qrevaddcl  9994  icoshft  10342  fznn  10445  sseqn  11228  pfxeq  11413  pfxsuffeqwrdeq  11415  pfxsuff1eqwrdeq  11416  shftdm  11532  2shfti  11541  sumeq2  12069  fsum3  12098  fsum2dlemstep  12145  prodeq2  12268  fprodseq  12294  bitsmod  12667  bitscmp  12669  gcdaddm  12705  grpidpropdg  13637  ismgmid  13640  gsumpropd2  13656  mhmpropd  13721  issubm2  13728  eqgid  13979  eqgabl  14083  rngpropd  14194  iscrng2  14258  ringpropd  14281  crngpropd  14282  crngunit  14356  dvdsrpropdg  14392  issubrg3  14493  lsslss  14655  lsspropdg  14705  znleval  14927  bastop2  15075  restopn2  15174  iscnp3  15194  lmbr2  15205  txlm  15270  ismet2  15345  xblpnfps  15389  xblpnf  15390  blininf  15415  blres  15425  elmopn2  15440  neibl  15482  metrest  15497  metcnp3  15502  metcnp  15503  metcnp2  15504  metcn  15505  txmetcn  15510  cnbl0  15525  cnblcld  15526  bl2ioo  15541  elcncf2  15565  cncfmet  15583  cnlimc  15663  lgsquadlem1  16076  lgsquadlem2  16077  2lgslem1a  16087  upgriswlkdc  16481  isclwwlknx  16537  clwwlkn1  16539  clwwlkn2  16542  eupth2lemsfi  16599