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  4212  reuhypd  4619  funbrfv2b  5750  dffn5im  5751  eqfnfv2  5810  fndmin  5819  fniniseg  5832  fmptco  5877  dff13  5977  riotabidva  6059  mpoeq123dva  6152  mpoeq3dva  6155  suppssrst  6505  suppssrgst  6506  suppinisegdc  6513  mpoxopovel  6517  qliftfun  6896  erovlem  6906  mapsnend  7105  xpcomco  7130  pw2f1odclem  7140  elfi2  7311  ctssdccl  7457  ltexpi  7710  dfplpq2  7727  axprecex  8253  zrevaddcl  9704  qrevaddcl  10059  icoshft  10408  fznn  10512  sseqn  11300  pfxeq  11489  pfxsuffeqwrdeq  11491  pfxsuff1eqwrdeq  11492  shftdm  11608  2shfti  11617  sumeq2  12149  fsum3  12178  fsum2dlemstep  12225  prodeq2  12348  fprodseq  12374  bitsmod  12747  bitscmp  12749  gcdaddm  12785  grpidpropdg  13752  ismgmid  13755  mhmpropd  13831  issubm2  13838  eqgid  14087  eqgabl  14223  rngpropd  14360  iscrng2  14425  ringpropd  14449  crngpropd  14450  crngunit  14526  dvdsrpropdg  14562  issubrg3  14663  lsslss  14826  lsspropdg  14876  znleval  15096  bastop2  15327  restopn2  15426  iscnp3  15446  lmbr2  15457  txlm  15522  ismet2  15597  xblpnfps  15641  xblpnf  15642  blininf  15667  blres  15677  elmopn2  15692  neibl  15734  metrest  15749  metcnp3  15754  metcnp  15755  metcnp2  15756  metcn  15757  txmetcn  15762  cnbl0  15777  cnblcld  15778  bl2ioo  15793  elcncf2  15817  cncfmet  15835  cnlimc  15915  lgsquadlem1  16418  lgsquadlem2  16419  2lgslem1a  16429  upgriswlkdc  16823  isclwwlknx  16879  clwwlkn1  16881  clwwlkn2  16884  eupth2lemsfi  16941