Theorem pm5.32da 456

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 454	1 |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  rexbida  2545  reubida  2734  rmobida  2740  mpteq12f  4211  reuhypd  4617  funbrfv2b  5747  dffn5im  5748  eqfnfv2  5807  fndmin  5816  fniniseg  5829  fmptco  5874  dff13  5974  riotabidva  6056  mpoeq123dva  6149  mpoeq3dva  6152  suppssrst  6501  suppssrgst  6502  mpoxopovel  6512  qliftfun  6891  erovlem  6901  mapsnend  7099  xpcomco  7124  pw2f1odclem  7134  elfi2  7306  ctssdccl  7451  ltexpi  7704  dfplpq2  7721  axprecex  8247  zrevaddcl  9699  qrevaddcl  10053  icoshft  10402  fznn  10506  sseqn  11293  pfxeq  11482  pfxsuffeqwrdeq  11484  pfxsuff1eqwrdeq  11485  shftdm  11601  2shfti  11610  sumeq2  12141  fsum3  12170  fsum2dlemstep  12217  prodeq2  12340  fprodseq  12366  bitsmod  12739  bitscmp  12741  gcdaddm  12777  grpidpropdg  13743  ismgmid  13746  mhmpropd  13822  issubm2  13829  eqgid  14078  eqgabl  14183  rngpropd  14303  iscrng2  14368  ringpropd  14392  crngpropd  14393  crngunit  14467  dvdsrpropdg  14503  issubrg3  14604  lsslss  14767  lsspropdg  14817  znleval  15037  bastop2  15234  restopn2  15333  iscnp3  15353  lmbr2  15364  txlm  15429  ismet2  15504  xblpnfps  15548  xblpnf  15549  blininf  15574  blres  15584  elmopn2  15599  neibl  15641  metrest  15656  metcnp3  15661  metcnp  15662  metcnp2  15663  metcn  15664  txmetcn  15669  cnbl0  15684  cnblcld  15685  bl2ioo  15700  elcncf2  15724  cncfmet  15742  cnlimc  15822  lgsquadlem1  16294  lgsquadlem2  16295  2lgslem1a  16305  upgriswlkdc  16699  isclwwlknx  16755  clwwlkn1  16757  clwwlkn2  16760  eupth2lemsfi  16817