Theorem pm5.74da 723

Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 4-May-2007.)

Hypothesis

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

Assertion

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

Proof of Theorem pm5.74da

Step	Hyp	Ref	Expression
1		pm5.74da.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
2	1	ex 450	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.74d 262	1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  ralbida  2982  ralbidva  2985  ralxpxfr2d  3327  elrab3t  3362  ordunisuc2  7044  dfom2  7067  pwfseqlem3  9482  lo1resb  14295  rlimresb  14296  o1resb  14297  fsumparts  14538  isprm3  15396  ramval  15712  islindf4  20177  cnntr  21079  fclsbas  21825  metcnp  22346  voliunlem3  23320  ellimc2  23641  limcflf  23645  mdegleb  23824  xrlimcnp  24695  dchrelbas3  24963  lmicom  25680  dmdbr5ati  29281  vtocl2d  29314  isarchi3  29741  cmpcref  29917  sscoid  32020  cdlemefrs29bpre0  35684  cdlemkid3N  36221  cdlemkid4  36222  hdmap1eulem  37113  hdmap1eulemOLDN  37114  jm2.25  37566  ntrneik2  38390  ntrneix2  38391  ntrneikb  38392  fourierdlem87  40410