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  3154  cbvraldva  3215  vtocl2d  3525  vtocl2  3529  vtocl3  3530  spc3egv  3566  ralxpxfr2d  3609  elabd2  3633  elrab3t  3655  csbie2df  4402  ordunisuc2  7800  dfom2  7824  pwfseqlem3  10589  lo1resb  15506  rlimresb  15507  o1resb  15508  fsumparts  15748  isprm3  16629  ramval  16955  islindf4  21723  cnntr  23138  fclsbas  23884  metcnp  24405  voliunlem3  25429  ellimc2  25754  limcflf  25758  mdegleb  25945  xrlimcnp  26854  dchrelbas3  27125  lmicom  28691  dmdbr5ati  32324  isarchi3  33114  islinds5  33311  cmpcref  33813  sscoid  35874  bj-equsalvwd  36741  cdlemefrs29bpre0  40363  cdlemkid3N  40900  cdlemkid4  40901  hdmap1eulem  41789  hdmap1eulemOLDN  41790  jm2.25  42961  ntrneik2  44054  ntrneix2  44055  ntrneikb  44056  fourierdlem87  46164