Theorem pm5.32da 452

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 450	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

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  2537  reubida  2725  rmobida  2731  mpteq12f  4189  reuhypd  4591  funbrfv2b  5720  dffn5im  5721  eqfnfv2  5775  fndmin  5784  fniniseg  5797  fmptco  5842  dff13  5940  riotabidva  6020  mpoeq123dva  6113  mpoeq3dva  6116  suppssrst  6460  suppssrgst  6461  mpoxopovel  6471  qliftfun  6850  erovlem  6860  mapsnend  7051  xpcomco  7076  pw2f1odclem  7086  elfi2  7258  ctssdccl  7401  ltexpi  7651  dfplpq2  7668  axprecex  8194  zrevaddcl  9627  qrevaddcl  9975  icoshft  10322  fznn  10422  sseqn  11199  pfxeq  11384  pfxsuffeqwrdeq  11386  pfxsuff1eqwrdeq  11387  shftdm  11503  2shfti  11512  sumeq2  12040  fsum3  12069  fsum2dlemstep  12116  prodeq2  12239  fprodseq  12265  bitsmod  12638  bitscmp  12640  gcdaddm  12676  grpidpropdg  13579  ismgmid  13582  gsumpropd2  13598  mhmpropd  13671  issubm2  13678  eqgid  13935  eqgabl  14039  rngpropd  14091  iscrng2  14151  ringpropd  14174  crngpropd  14175  crngunit  14248  dvdsrpropdg  14284  issubrg3  14384  lsslss  14521  lsspropdg  14571  znleval  14793  bastop2  14941  restopn2  15040  iscnp3  15060  lmbr2  15071  txlm  15136  ismet2  15211  xblpnfps  15255  xblpnf  15256  blininf  15281  blres  15291  elmopn2  15306  neibl  15348  metrest  15363  metcnp3  15368  metcnp  15369  metcnp2  15370  metcn  15371  txmetcn  15376  cnbl0  15391  cnblcld  15392  bl2ioo  15407  elcncf2  15431  cncfmet  15449  cnlimc  15529  lgsquadlem1  15942  lgsquadlem2  15943  2lgslem1a  15953  upgriswlkdc  16347  isclwwlknx  16403  clwwlkn1  16405  clwwlkn2  16408  eupth2lemsfi  16465