Theorem pm5.74da 804

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  cbvaldvaw  2037  sb4b  2480  ralbidva  3176  cbvraldva  3239  ralbidaOLD  3271  vtocl2d  3562  vtocl2  3566  vtocl3  3567  spc3egv  3603  ralxpxfr2d  3646  elabd2  3670  elrab3t  3691  csbie2df  4443  ordunisuc2  7865  dfom2  7889  pwfseqlem3  10700  lo1resb  15600  rlimresb  15601  o1resb  15602  fsumparts  15842  isprm3  16720  ramval  17046  islindf4  21858  cnntr  23283  fclsbas  24029  metcnp  24554  voliunlem3  25587  ellimc2  25912  limcflf  25916  mdegleb  26103  xrlimcnp  27011  dchrelbas3  27282  lmicom  28796  dmdbr5ati  32441  isarchi3  33194  islinds5  33395  cmpcref  33849  sscoid  35914  bj-equsalvwd  36781  cdlemefrs29bpre0  40398  cdlemkid3N  40935  cdlemkid4  40936  hdmap1eulem  41824  hdmap1eulemOLDN  41825  jm2.25  43011  ntrneik2  44105  ntrneix2  44106  ntrneikb  44107  fourierdlem87  46208