Theorem pm5.32da 456

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 9-Dec-2006.)

Hypothesis

Ref	Expression
pm5.32da.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
pm5.32da	⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Proof of Theorem pm5.32da

Step	Hyp	Ref	Expression
1		pm5.32da.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
2	1	ex 115	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.32d 454	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

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  7104  xpcomco  7129  pw2f1odclem  7139  elfi2  7312  ctssdccl  7458  ltexpi  7711  dfplpq2  7728  axprecex  8254  zrevaddcl  9707  qrevaddcl  10061  icoshft  10410  fznn  10514  sseqn  11302  pfxeq  11491  pfxsuffeqwrdeq  11493  pfxsuff1eqwrdeq  11494  shftdm  11610  2shfti  11619  sumeq2  12151  fsum3  12180  fsum2dlemstep  12227  prodeq2  12350  fprodseq  12376  bitsmod  12749  bitscmp  12751  gcdaddm  12787  grpidpropdg  13754  ismgmid  13757  mhmpropd  13833  issubm2  13840  eqgid  14089  eqgabl  14225  rngpropd  14362  iscrng2  14427  ringpropd  14451  crngpropd  14452  crngunit  14528  dvdsrpropdg  14564  issubrg3  14665  lsslss  14828  lsspropdg  14878  znleval  15098  bastop2  15322  restopn2  15421  iscnp3  15441  lmbr2  15452  txlm  15517  ismet2  15592  xblpnfps  15636  xblpnf  15637  blininf  15662  blres  15672  elmopn2  15687  neibl  15729  metrest  15744  metcnp3  15749  metcnp  15750  metcnp2  15751  metcn  15752  txmetcn  15757  cnbl0  15772  cnblcld  15773  bl2ioo  15788  elcncf2  15812  cncfmet  15830  cnlimc  15910  lgsquadlem1  16413  lgsquadlem2  16414  2lgslem1a  16424  upgriswlkdc  16818  isclwwlknx  16874  clwwlkn1  16876  clwwlkn2  16879  eupth2lemsfi  16936