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  mpoxopovel  6516  qliftfun  6895  erovlem  6905  mapsnend  7103  xpcomco  7128  pw2f1odclem  7138  elfi2  7311  ctssdccl  7457  ltexpi  7710  dfplpq2  7727  axprecex  8253  zrevaddcl  9706  qrevaddcl  10060  icoshft  10409  fznn  10513  sseqn  11301  pfxeq  11490  pfxsuffeqwrdeq  11492  pfxsuff1eqwrdeq  11493  shftdm  11609  2shfti  11618  sumeq2  12150  fsum3  12179  fsum2dlemstep  12226  prodeq2  12349  fprodseq  12375  bitsmod  12748  bitscmp  12750  gcdaddm  12786  grpidpropdg  13753  ismgmid  13756  mhmpropd  13832  issubm2  13839  eqgid  14088  eqgabl  14224  rngpropd  14361  iscrng2  14426  ringpropd  14450  crngpropd  14451  crngunit  14527  dvdsrpropdg  14563  issubrg3  14664  lsslss  14827  lsspropdg  14877  znleval  15097  bastop2  15310  restopn2  15409  iscnp3  15429  lmbr2  15440  txlm  15505  ismet2  15580  xblpnfps  15624  xblpnf  15625  blininf  15650  blres  15660  elmopn2  15675  neibl  15717  metrest  15732  metcnp3  15737  metcnp  15738  metcnp2  15739  metcn  15740  txmetcn  15745  cnbl0  15760  cnblcld  15761  bl2ioo  15776  elcncf2  15800  cncfmet  15818  cnlimc  15898  lgsquadlem1  16401  lgsquadlem2  16402  2lgslem1a  16412  upgriswlkdc  16806  isclwwlknx  16862  clwwlkn1  16864  clwwlkn2  16867  eupth2lemsfi  16924