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  2415  2sb6rf  2471  sbcom3  2504  moeu  2576  ralbiia  3073  ceqsal  3485  ceqsalv  3487  ceqsralv  3488  clel2g  3625  clel4g  3629  dfdif3OLD  4081  csbie2df  4406  rabeqsnd  4633  ralsng  4639  snssb  4746  frinxp  5721  idrefALT  6084  dfom2  7844  dfacacn  10095  kmlem8  10111  kmlem13  10116  kmlem14  10117  axgroth2  10778  bnj1171  34990  bnj1253  35007  orbi2iALT  35672  filnetlem4  36369  wl-equsalvw  37526  lcmineqlem4  42020  dvrelog2b  42054  aks6d1c1  42104  aks6d1c4  42112  aks6d1c6lem3  42160  elintima  43642  ichexmpl2  47471