Theorem pm5.74da 791

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  sb4b  2421  ralbidva  3140  ralbida  3171  vtocl2  3474  vtocl3  3476  spc3egv  3516  ralxpxfr2d  3548  elrab3t  3588  ordunisuc2  7369  dfom2  7392  pwfseqlem3  9872  lo1resb  14772  rlimresb  14773  o1resb  14774  fsumparts  15011  isprm3  15873  ramval  16190  islindf4  20674  cnntr  21577  fclsbas  22323  metcnp  22844  voliunlem3  23846  ellimc2  24168  limcflf  24172  mdegleb  24351  xrlimcnp  25238  dchrelbas3  25506  lmicom  26266  dmdbr5ati  29970  vtocl2d  30003  isarchi3  30438  islinds5  30561  cmpcref  30715  sscoid  32835  cdlemefrs29bpre0  36925  cdlemkid3N  37462  cdlemkid4  37463  hdmap1eulem  38351  hdmap1eulemOLDN  38352  jm2.25  38937  ntrneik2  39750  ntrneix2  39751  ntrneikb  39752  fourierdlem87  41855