Theorem pm5.74i 270

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bitrd  278  imbi2i  335  bibi2d  341  ibib  366  ibibr  367  pm5.4  387  pm5.42  542  anclb  544  ancrb  546  pm5.3  571  cases2  1044  cador  1607  equsalvw  2005  ax13b  2033  sbcom3vv  2096  equsalv  2256  equsal  2414  2sb6rf  2470  sbcom3  2503  moeu  2575  ralbiia  3089  ceqsal  3508  ceqsalv  3510  ceqsralv  3512  clel2g  3646  clel4g  3651  elabg  3665  dfdif3  4113  csbie2df  4439  rabeqsnd  4670  ralsng  4676  snssb  4785  frinxp  5757  idrefALT  6111  dfom2  7859  dfacacn  10138  kmlem8  10154  kmlem13  10159  kmlem14  10160  axgroth2  10822  bnj1171  34309  bnj1253  34326  filnetlem4  35569  wl-equsalvw  36710  lcmineqlem4  41203  dvrelog2b  41237  elintima  42706  ichexmpl2  46436