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  2503  reubida  2690  rmobida  2696  mpteq12f  4140  reuhypd  4536  funbrfv2b  5646  dffn5im  5647  eqfnfv2  5701  fndmin  5710  fniniseg  5723  rexsupp  5727  fmptco  5769  dff13  5860  riotabidva  5939  mpoeq123dva  6029  mpoeq3dva  6032  mpoxopovel  6350  qliftfun  6727  erovlem  6737  xpcomco  6946  pw2f1odclem  6956  elfi2  7100  ctssdccl  7239  ltexpi  7485  dfplpq2  7502  axprecex  8028  zrevaddcl  9458  qrevaddcl  9800  icoshft  10147  fznn  10246  pfxeq  11187  pfxsuffeqwrdeq  11189  pfxsuff1eqwrdeq  11190  shftdm  11248  2shfti  11257  sumeq2  11785  fsum3  11813  fsum2dlemstep  11860  prodeq2  11983  fprodseq  12009  bitsmod  12382  bitscmp  12384  gcdaddm  12420  grpidpropdg  13321  ismgmid  13324  gsumpropd2  13340  mhmpropd  13413  issubm2  13420  eqgid  13677  eqgabl  13781  rngpropd  13832  iscrng2  13892  ringpropd  13915  crngpropd  13916  crngunit  13988  dvdsrpropdg  14024  issubrg3  14124  lsslss  14258  lsspropdg  14308  znleval  14530  bastop2  14671  restopn2  14770  iscnp3  14790  lmbr2  14801  txlm  14866  ismet2  14941  xblpnfps  14985  xblpnf  14986  blininf  15011  blres  15021  elmopn2  15036  neibl  15078  metrest  15093  metcnp3  15098  metcnp  15099  metcnp2  15100  metcn  15101  txmetcn  15106  cnbl0  15121  cnblcld  15122  bl2ioo  15137  elcncf2  15161  cncfmet  15179  cnlimc  15259  lgsquadlem1  15669  lgsquadlem2  15670  2lgslem1a  15680