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  1605  equsalvw  2003  ax13b  2031  sbbiiev  2092  equsalv  2268  equsal  2425  2sb6rf  2481  sbcom3  2514  moeu  2586  ralbiia  3097  ceqsal  3527  ceqsalv  3529  ceqsralv  3531  clel2g  3672  clel4g  3676  elabg  3690  dfdif3OLD  4141  csbie2df  4466  rabeqsnd  4691  ralsng  4697  snssb  4807  frinxp  5782  idrefALT  6143  dfom2  7905  dfacacn  10211  kmlem8  10227  kmlem13  10232  kmlem14  10233  axgroth2  10894  bnj1171  34976  bnj1253  34993  orbi2iALT  35653  filnetlem4  36347  wl-equsalvw  37492  lcmineqlem4  41989  dvrelog2b  42023  aks6d1c1  42073  aks6d1c4  42081  aks6d1c6lem3  42129  elintima  43615  ichexmpl2  47344