Theorem pm5.74da 719

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  ralbida  2965  ralbidva  2968  ralxpxfr2d  3298  elrab3t  3330  ordunisuc2  6936  dfom2  6959  pwfseqlem3  9361  lo1resb  14143  rlimresb  14144  o1resb  14145  fsumparts  14379  isprm3  15234  ramval  15550  islindf4  19996  cnntr  20889  fclsbas  21635  metcnp  22156  voliunlem3  23127  ellimc2  23447  limcflf  23451  mdegleb  23628  xrlimcnp  24495  dchrelbas3  24763  lmicom  25480  dmdbr5ati  28665  vtocl2d  28699  isarchi3  29072  cmpcref  29245  sscoid  31190  cdlemefrs29bpre0  34702  cdlemkid3N  35239  cdlemkid4  35240  hdmap1eulem  36131  hdmap1eulemOLDN  36132  jm2.25  36584  ntrneik2  37410  ntrneix2  37411  ntrneikb  37412  fourierdlem87  39086