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  1047  cador  1609  equsalvw  2005  ax13b  2033  sbbiiev  2097  equsalv  2272  equsal  2419  2sb6rf  2475  sbcom3  2508  moeu  2580  ralbiia  3077  ceqsal  3475  ceqsalv  3477  ceqsralv  3478  clel2g  3610  clel4g  3614  dfdif3OLD  4067  csbie2df  4392  rabeqsnd  4623  ralsng  4629  snssb  4736  frinxp  5704  idrefALT  6066  dfom2  7806  dfacacn  10042  kmlem8  10058  kmlem13  10063  kmlem14  10064  axgroth2  10725  bnj1171  35035  bnj1253  35052  orbi2iALT  35752  filnetlem4  36448  wl-equsalvw  37605  lcmineqlem4  42148  dvrelog2b  42182  aks6d1c1  42232  aks6d1c4  42240  aks6d1c6lem3  42288  elintima  43773  ichexmpl2  47597