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  2034  sb4b  2477  ralbidva  3173  cbvraldva  3236  ralbidaOLD  3268  vtocl2d  3561  vtocl2  3565  vtocl3  3566  spc3egv  3602  ralxpxfr2d  3645  elabd2  3669  elrab3t  3693  csbie2df  4448  ordunisuc2  7864  dfom2  7888  pwfseqlem3  10697  lo1resb  15596  rlimresb  15597  o1resb  15598  fsumparts  15838  isprm3  16716  ramval  17041  islindf4  21875  cnntr  23298  fclsbas  24044  metcnp  24569  voliunlem3  25600  ellimc2  25926  limcflf  25930  mdegleb  26117  xrlimcnp  27025  dchrelbas3  27296  lmicom  28810  dmdbr5ati  32450  isarchi3  33176  islinds5  33374  cmpcref  33810  sscoid  35894  bj-equsalvwd  36762  cdlemefrs29bpre0  40378  cdlemkid3N  40915  cdlemkid4  40916  hdmap1eulem  41804  hdmap1eulemOLDN  41805  jm2.25  42987  ntrneik2  44081  ntrneix2  44082  ntrneikb  44083  fourierdlem87  46148