Theorem pm5.74i 270

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 269	. 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)))
3	1, 2	mpbi 229	1 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bitrd  278  imbi2i  335  bibi2d  342  ibib  367  ibibr  368  pm5.4  389  pm5.42  543  anclb  545  ancrb  547  pm5.3  572  cases2  1044  cador  1611  equsalvw  2008  ax13b  2036  sbcom3vv  2100  equsalv  2262  equsal  2417  2sb6rf  2473  sbcom3  2510  moeu  2583  ralbiia  3089  ceqsalv  3457  ceqsralv  3459  clel2g  3581  clel4g  3586  elabg  3600  dfdif3  4045  csbie2df  4371  ralsng  4606  frinxp  5660  idrefALT  6007  dfom2  7689  dfacacn  9828  kmlem8  9844  kmlem13  9849  kmlem14  9850  axgroth2  10512  rabeqsnd  30749  bnj1171  32880  bnj1253  32897  filnetlem4  34497  wl-equsalvw  35624  lcmineqlem4  39968  dvrelog2b  40002  elintima  41150  ichexmpl2  44810