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  2301  equsal  2446  2sb6rf  2502  sbcom3  2535  moeu  2608  ralbiia  3106  ceqsal  3487  ceqsalv  3489  ceqsralv  3490  clel2g  3613  clel4g  3617  csbie2df  4401  rabeqsnd  4630  ralsng  4636  snssb  4743  frinxp  5738  idrefALT  6107  dfom2  7864  dfacacn  10144  kmlem8  10160  kmlem13  10165  kmlem14  10166  axgroth2  10834  bnj1171  35509  bnj1253  35526  orbi2iALT  36264  filnetlem4  37000  mh-regprimbi  37164  mh-infprim1bi  37165  wl-equsalvw  38301  qmapeldisjsim  39608  lcmineqlem4  42898  dvrelog2b  42932  aks6d1c1  42982  aks6d1c4  42990  aks6d1c6lem3  43038  elintima  44493  ichexmpl2  48370