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  1608  equsalvw  2004  ax13b  2032  sbbiiev  2093  equsalv  2268  equsal  2416  2sb6rf  2472  sbcom3  2505  moeu  2577  ralbiia  3074  ceqsal  3488  ceqsalv  3490  ceqsralv  3491  clel2g  3628  clel4g  3632  dfdif3OLD  4084  csbie2df  4409  rabeqsnd  4636  ralsng  4642  snssb  4749  frinxp  5724  idrefALT  6087  dfom2  7847  dfacacn  10102  kmlem8  10118  kmlem13  10123  kmlem14  10124  axgroth2  10785  bnj1171  34997  bnj1253  35014  orbi2iALT  35679  filnetlem4  36376  wl-equsalvw  37533  lcmineqlem4  42027  dvrelog2b  42061  aks6d1c1  42111  aks6d1c4  42119  aks6d1c6lem3  42167  elintima  43649  ichexmpl2  47475