Theorem pm5.74da 804

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 416	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.74d 276	1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  cbvaldvaw  2048  sb4b  2474  sb4bOLD  2475  ralbidva  3107  ralbida  3143  vtocl2d  3462  vtocl2  3466  vtocl3  3467  spc3egv  3508  ralxpxfr2d  3543  elabd2  3569  elrab3t  3590  csbie2df  4341  ordunisuc2  7601  dfom2  7624  pwfseqlem3  10239  lo1resb  15090  rlimresb  15091  o1resb  15092  fsumparts  15333  isprm3  16203  ramval  16524  islindf4  20754  cnntr  22126  fclsbas  22872  metcnp  23393  voliunlem3  24403  ellimc2  24728  limcflf  24732  mdegleb  24916  xrlimcnp  25805  dchrelbas3  26073  lmicom  26833  dmdbr5ati  30457  isarchi3  31114  islinds5  31231  cmpcref  31468  sscoid  33901  bj-equsalvwd  34648  cdlemefrs29bpre0  38096  cdlemkid3N  38633  cdlemkid4  38634  hdmap1eulem  39522  hdmap1eulemOLDN  39523  jm2.25  40465  ntrneik2  41320  ntrneix2  41321  ntrneikb  41322  fourierdlem87  43352