Theorem pm5.74da 816

Description: Distribution of implication over biconditional (deduction form). Variant of pm5.74d 276. (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 418	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.74d 276	1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  cbvaldvaw  2070  sb4b  2504  ralbidva  3183  cbvraldva  3242  vtocl2d  3523  vtocl2  3526  vtocl3  3527  spc3egv  3557  ralxpxfr2d  3599  elabd2  3623  elrab3t  3643  csbie2df  4400  ordunisuc2  7856  dfom2  7880  pwfseqlem3  10749  lo1resb  15737  rlimresb  15738  o1resb  15739  fsumparts  15979  isprm3  16864  ramval  17192  islindf4  22150  cnntr  23599  fclsbas  24346  metcnp  24866  voliunlem3  25879  ellimc2  26203  limcflf  26207  mdegleb  26388  xrlimcnp  27302  dchrelbas3  27571  elplng  29264  plngcplem  29269  lmicom  29299  dmdbr5ati  33030  isarchi3  33795  islinds5  33970  cmpcref  34529  sscoid  36768  regsfromregtco  37419  bj-equsalvwd  37767  cdlemefrs29bpre0  41547  cdlemkid3N  42084  cdlemkid4  42085  hdmap1eulem  42973  hdmap1eulemOLDN  42974  jm2.25  44100  ntrneik2  45186  ntrneix2  45187  ntrneikb  45188  fourierdlem87  47297