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  2421  2sb6rf  2477  sbcom3  2510  moeu  2583  ralbiia  3081  ceqsal  3467  ceqsalv  3469  ceqsralv  3470  clel2g  3601  clel4g  3605  dfdif3OLD  4058  csbie2df  4383  rabeqsnd  4613  ralsng  4619  snssb  4726  frinxp  5714  idrefALT  6076  dfom2  7819  dfacacn  10064  kmlem8  10080  kmlem13  10085  kmlem14  10086  axgroth2  10748  bnj1171  35142  bnj1253  35159  orbi2iALT  35867  filnetlem4  36563  mh-regprimbi  36727  mh-infprim1bi  36728  wl-equsalvw  37863  qmapeldisjsim  39181  lcmineqlem4  42471  dvrelog2b  42505  aks6d1c1  42555  aks6d1c4  42563  aks6d1c6lem3  42611  elintima  44080  ichexmpl2  47930