Theorem pm5.74da 815

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

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

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 401

This theorem is referenced by:  cbvaldvaw  2068  sb4b  2507  ralbidva  3186  cbvraldva  3245  vtocl2d  3528  vtocl2  3531  vtocl3  3532  spc3egv  3562  ralxpxfr2d  3605  elabd2  3629  elrab3t  3649  csbie2df  4408  ordunisuc2  7836  dfom2  7860  pwfseqlem3  10640  lo1resb  15611  rlimresb  15612  o1resb  15613  fsumparts  15854  isprm3  16736  ramval  17063  islindf4  21988  cnntr  23432  fclsbas  24178  metcnp  24698  voliunlem3  25711  ellimc2  26036  limcflf  26040  mdegleb  26221  xrlimcnp  27133  dchrelbas3  27402  elplng  29062  plngcplem  29067  lmicom  29097  dmdbr5ati  32774  isarchi3  33507  islinds5  33682  cmpcref  34240  sscoid  36403  regsfromregtco  37049  bj-equsalvwd  37397  cdlemefrs29bpre0  41170  cdlemkid3N  41707  cdlemkid4  41708  hdmap1eulem  42596  hdmap1eulemOLDN  42597  jm2.25  43726  ntrneik2  44818  ntrneix2  44819  ntrneikb  44820  fourierdlem87  46907