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  1048  cador  1610  equsalvw  2006  ax13b  2034  sbbiiev  2098  equsalv  2275  equsal  2422  2sb6rf  2478  sbcom3  2511  moeu  2584  ralbiia  3082  ceqsal  3468  ceqsalv  3470  ceqsralv  3471  clel2g  3602  clel4g  3606  dfdif3OLD  4059  csbie2df  4384  rabeqsnd  4614  ralsng  4620  snssb  4727  frinxp  5707  idrefALT  6070  dfom2  7812  dfacacn  10055  kmlem8  10071  kmlem13  10076  kmlem14  10077  axgroth2  10739  bnj1171  35158  bnj1253  35175  orbi2iALT  35883  filnetlem4  36579  mh-regprimbi  36743  mh-infprim1bi  36744  wl-equsalvw  37877  qmapeldisjsim  39195  lcmineqlem4  42485  dvrelog2b  42519  aks6d1c1  42569  aks6d1c4  42577  aks6d1c6lem3  42625  elintima  44098  ichexmpl2  47942