Theorem pm5.74i 271

Description: Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.)

Hypothesis

Ref	Expression
pm5.74i.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
pm5.74i	⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))

Proof of Theorem pm5.74i

Step	Hyp	Ref	Expression
1		pm5.74i.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		pm5.74 270	. 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)))
3	1, 2	mpbi 230	1 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 206

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

This theorem is referenced by:  bitrd  279  imbi2i  336  bibi2d  342  ibib  367  ibibr  368  pm5.4  388  pm5.42  543  anclb  545  ancrb  547  pm5.3  572  cases2  1047  cador  1608  equsalvw  2004  ax13b  2032  sbbiiev  2093  equsalv  2268  equsal  2415  2sb6rf  2471  sbcom3  2504  moeu  2576  ralbiia  3073  ceqsal  3476  ceqsalv  3478  ceqsralv  3479  clel2g  3616  clel4g  3620  dfdif3OLD  4071  csbie2df  4396  rabeqsnd  4623  ralsng  4629  snssb  4736  frinxp  5706  idrefALT  6066  dfom2  7808  dfacacn  10055  kmlem8  10071  kmlem13  10076  kmlem14  10077  axgroth2  10738  bnj1171  34969  bnj1253  34986  orbi2iALT  35660  filnetlem4  36357  wl-equsalvw  37514  lcmineqlem4  42008  dvrelog2b  42042  aks6d1c1  42092  aks6d1c4  42100  aks6d1c6lem3  42148  elintima  43629  ichexmpl2  47458