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  1608  equsalvw  2003  ax13b  2031  sbbiiev  2092  equsalv  2267  equsal  2422  2sb6rf  2478  sbcom3  2511  moeu  2583  ralbiia  3091  ceqsal  3519  ceqsalv  3521  ceqsralv  3522  clel2g  3659  clel4g  3663  elabg  3676  dfdif3OLD  4118  csbie2df  4443  rabeqsnd  4669  ralsng  4675  snssb  4782  frinxp  5768  idrefALT  6131  dfom2  7889  dfacacn  10182  kmlem8  10198  kmlem13  10203  kmlem14  10204  axgroth2  10865  bnj1171  35014  bnj1253  35031  orbi2iALT  35690  filnetlem4  36382  wl-equsalvw  37539  lcmineqlem4  42033  dvrelog2b  42067  aks6d1c1  42117  aks6d1c4  42125  aks6d1c6lem3  42173  elintima  43666  ichexmpl2  47457