Theorem pm5.74i 273

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bitrd  281  imbi2i  338  bibi2d  344  ibib  369  ibibr  370  pm5.4  391  pm5.42  551  anclb  553  ancrb  555  pm5.3  580  cases2  1058  cador  1627  equsalvw  2023  ax13b  2051  sbbiiev  2125  equsalv  2301  equsal  2447  2sb6rf  2503  sbcom3  2536  moeu  2609  ralbiia  3105  ceqsal  3490  ceqsalv  3492  ceqsralv  3493  clel2g  3617  clel4g  3621  dfdif3OLD  4070  csbie2df  4394  rabeqsnd  4625  ralsng  4631  snssb  4738  frinxp  5726  idrefALT  6096  dfom2  7843  dfacacn  10092  kmlem8  10108  kmlem13  10113  kmlem14  10114  axgroth2  10777  bnj1171  35256  bnj1253  35273  orbi2iALT  35996  filnetlem4  36702  mh-regprimbi  36866  mh-infprim1bi  36867  wl-equsalvw  38002  qmapeldisjsim  39320  lcmineqlem4  42610  dvrelog2b  42644  aks6d1c1  42694  aks6d1c4  42702  aks6d1c6lem3  42750  elintima  44190  ichexmpl2  48037