Theorem pm5.74da 803

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  2038  sb4b  2473  ralbidva  3150  cbvraldva  3209  vtocl2d  3519  vtocl2  3523  vtocl3  3524  spc3egv  3560  ralxpxfr2d  3603  elabd2  3627  elrab3t  3649  csbie2df  4396  ordunisuc2  7784  dfom2  7808  pwfseqlem3  10573  lo1resb  15490  rlimresb  15491  o1resb  15492  fsumparts  15732  isprm3  16613  ramval  16939  islindf4  21764  cnntr  23179  fclsbas  23925  metcnp  24446  voliunlem3  25470  ellimc2  25795  limcflf  25799  mdegleb  25986  xrlimcnp  26895  dchrelbas3  27166  lmicom  28752  dmdbr5ati  32385  isarchi3  33148  islinds5  33323  cmpcref  33836  sscoid  35906  bj-equsalvwd  36773  cdlemefrs29bpre0  40395  cdlemkid3N  40932  cdlemkid4  40933  hdmap1eulem  41821  hdmap1eulemOLDN  41822  jm2.25  42992  ntrneik2  44085  ntrneix2  44086  ntrneikb  44087  fourierdlem87  46194