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  1640  equsalvw  2036  ax13b  2064  sbbiiev  2129  equsalv  2301  equsal  2446  2sb6rf  2502  sbcom3  2535  moeu  2608  ralbiia  3106  ceqsal  3487  ceqsalv  3489  ceqsralv  3490  clel2g  3612  clel4g  3616  csbie2df  4400  rabeqsnd  4626  ralsng  4632  snssb  4739  frinxp  5734  idrefALT  6108  dfom2  7881  dfacacn  10225  kmlem8  10241  kmlem13  10246  kmlem14  10247  axgroth2  10915  bnj1171  35678  bnj1253  35695  orbi2iALT  36538  filnetlem4  37263  mh-regprimbi  37427  mh-infprim1bi  37428  wl-equsalvw  38577  qmapeldisjsim  39899  lcmineqlem4  43189  dvrelog2b  43223  aks6d1c1  43273  aks6d1c4  43281  aks6d1c6lem3  43329  elintima  44760  ichexmpl2  48659