Theorem pm5.74i 271

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bitrd  279  imbi2i  336  bibi2d  342  ibib  367  ibibr  368  pm5.4  388  pm5.42  543  anclb  545  ancrb  547  pm5.3  572  cases2  1047  cador  1609  equsalvw  2005  ax13b  2033  sbbiiev  2095  equsalv  2270  equsal  2417  2sb6rf  2473  sbcom3  2506  moeu  2578  ralbiia  3076  ceqsal  3474  ceqsalv  3476  ceqsralv  3477  clel2g  3614  clel4g  3618  dfdif3OLD  4068  csbie2df  4393  rabeqsnd  4622  ralsng  4628  snssb  4735  frinxp  5699  idrefALT  6060  dfom2  7798  dfacacn  10033  kmlem8  10049  kmlem13  10054  kmlem14  10055  axgroth2  10716  bnj1171  35010  bnj1253  35027  orbi2iALT  35727  filnetlem4  36421  wl-equsalvw  37578  lcmineqlem4  42071  dvrelog2b  42105  aks6d1c1  42155  aks6d1c4  42163  aks6d1c6lem3  42211  elintima  43692  ichexmpl2  47507