Theorem pm5.74i 274

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bitrd  282  imbi2i  339  bibi2d  345  ibib  370  ibibr  371  pm5.4  393  pm5.42  553  anclb  555  ancrb  557  pm5.3  583  cases2  1063  cador  1641  equsalvw  2037  ax13b  2065  sbbiiev  2130  equsalv  2305  equsal  2451  2sb6rf  2507  sbcom3  2540  moeu  2613  ralbiia  3111  ceqsal  3494  ceqsalv  3496  ceqsralv  3497  clel2g  3620  clel4g  3624  csbie2df  4408  rabeqsnd  4637  ralsng  4643  snssb  4750  frinxp  5746  idrefALT  6115  dfom2  7870  dfacacn  10141  kmlem8  10157  kmlem13  10162  kmlem14  10163  axgroth2  10825  bnj1171  35453  bnj1253  35470  orbi2iALT  36214  filnetlem4  36949  mh-regprimbi  37113  mh-infprim1bi  37114  wl-equsalvw  38250  qmapeldisjsim  39567  lcmineqlem4  42857  dvrelog2b  42891  aks6d1c1  42941  aks6d1c4  42949  aks6d1c6lem3  42997  elintima  44437  ichexmpl2  48277