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  2003  ax13b  2031  sbbiiev  2092  equsalv  2267  equsal  2421  2sb6rf  2477  sbcom3  2510  moeu  2582  ralbiia  3080  ceqsal  3498  ceqsalv  3500  ceqsralv  3501  clel2g  3638  clel4g  3642  elabg  3655  dfdif3OLD  4093  csbie2df  4418  rabeqsnd  4645  ralsng  4651  snssb  4758  frinxp  5737  idrefALT  6100  dfom2  7863  dfacacn  10156  kmlem8  10172  kmlem13  10177  kmlem14  10178  axgroth2  10839  bnj1171  35031  bnj1253  35048  orbi2iALT  35707  filnetlem4  36399  wl-equsalvw  37556  lcmineqlem4  42045  dvrelog2b  42079  aks6d1c1  42129  aks6d1c4  42137  aks6d1c6lem3  42185  elintima  43677  ichexmpl2  47484