Theorem pm5.74da 801

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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  cbvaldvaw  2040  sb4b  2473  ralbidva  3174  cbvraldva  3235  ralbidaOLD  3267  vtocl2d  3549  vtocl2  3554  vtocl3  3555  spc3egv  3593  ralxpxfr2d  3634  elabd2  3660  elrab3t  3682  csbie2df  4440  ordunisuc2  7837  dfom2  7861  pwfseqlem3  10659  lo1resb  15513  rlimresb  15514  o1resb  15515  fsumparts  15757  isprm3  16625  ramval  16946  islindf4  21613  cnntr  23000  fclsbas  23746  metcnp  24271  voliunlem3  25302  ellimc2  25627  limcflf  25631  mdegleb  25818  xrlimcnp  26710  dchrelbas3  26978  lmicom  28307  dmdbr5ati  31943  isarchi3  32604  islinds5  32755  cmpcref  33129  sscoid  35190  bj-equsalvwd  35962  cdlemefrs29bpre0  39571  cdlemkid3N  40108  cdlemkid4  40109  hdmap1eulem  40997  hdmap1eulemOLDN  40998  jm2.25  42041  ntrneik2  43146  ntrneix2  43147  ntrneikb  43148  fourierdlem87  45208