Theorem pm5.32da 448

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 114	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.32d 446	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  rexbida  2452  reubida  2638  rmobida  2643  mpteq12f  4044  reuhypd  4431  funbrfv2b  5513  dffn5im  5514  eqfnfv2  5566  fndmin  5574  fniniseg  5587  rexsupp  5591  fmptco  5633  dff13  5718  riotabidva  5796  mpoeq123dva  5882  mpoeq3dva  5885  mpoxopovel  6188  qliftfun  6562  erovlem  6572  xpcomco  6771  elfi2  6916  ctssdccl  7055  ltexpi  7257  dfplpq2  7274  axprecex  7800  zrevaddcl  9217  qrevaddcl  9553  icoshft  9894  fznn  9991  shftdm  10722  2shfti  10731  sumeq2  11256  fsum3  11284  fsum2dlemstep  11331  prodeq2  11454  fprodseq  11480  gcdaddm  11868  bastop2  12495  restopn2  12594  iscnp3  12614  lmbr2  12625  txlm  12690  ismet2  12765  xblpnfps  12809  xblpnf  12810  blininf  12835  blres  12845  elmopn2  12860  neibl  12902  metrest  12917  metcnp3  12922  metcnp  12923  metcnp2  12924  metcn  12925  txmetcn  12930  cnbl0  12945  cnblcld  12946  bl2ioo  12953  elcncf2  12972  cncfmet  12990  cnlimc  13052