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  2433  reubida  2615  rmobida  2620  mpteq12f  4016  reuhypd  4400  funbrfv2b  5474  dffn5im  5475  eqfnfv2  5527  fndmin  5535  fniniseg  5548  rexsupp  5552  fmptco  5594  dff13  5677  riotabidva  5754  mpoeq123dva  5840  mpoeq3dva  5843  mpoxopovel  6146  qliftfun  6519  erovlem  6529  xpcomco  6728  elfi2  6868  ctssdccl  7004  ltexpi  7169  dfplpq2  7186  axprecex  7712  zrevaddcl  9128  qrevaddcl  9463  icoshft  9803  fznn  9900  shftdm  10626  2shfti  10635  sumeq2  11160  fsum3  11188  fsum2dlemstep  11235  prodeq2  11358  fprodseq  11384  gcdaddm  11708  bastop2  12292  restopn2  12391  iscnp3  12411  lmbr2  12422  txlm  12487  ismet2  12562  xblpnfps  12606  xblpnf  12607  blininf  12632  blres  12642  elmopn2  12657  neibl  12699  metrest  12714  metcnp3  12719  metcnp  12720  metcnp2  12721  metcn  12722  txmetcn  12727  cnbl0  12742  cnblcld  12743  bl2ioo  12750  elcncf2  12769  cncfmet  12787  cnlimc  12849