Theorem pm5.32da 447

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 445	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  2432  reubida  2612  rmobida  2617  mpteq12f  4008  reuhypd  4392  funbrfv2b  5466  dffn5im  5467  eqfnfv2  5519  fndmin  5527  fniniseg  5540  rexsupp  5544  fmptco  5586  dff13  5669  riotabidva  5746  mpoeq123dva  5832  mpoeq3dva  5835  mpoxopovel  6138  qliftfun  6511  erovlem  6521  xpcomco  6720  elfi2  6860  ctssdccl  6996  ltexpi  7145  dfplpq2  7162  axprecex  7688  zrevaddcl  9104  qrevaddcl  9436  icoshft  9773  fznn  9869  shftdm  10594  2shfti  10603  sumeq2  11128  fsum3  11156  fsum2dlemstep  11203  prodeq2  11326  gcdaddm  11672  bastop2  12253  restopn2  12352  iscnp3  12372  lmbr2  12383  txlm  12448  ismet2  12523  xblpnfps  12567  xblpnf  12568  blininf  12593  blres  12603  elmopn2  12618  neibl  12660  metrest  12675  metcnp3  12680  metcnp  12681  metcnp2  12682  metcn  12683  txmetcn  12688  cnbl0  12703  cnblcld  12704  bl2ioo  12711  elcncf2  12730  cncfmet  12748  cnlimc  12810