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  2097  equsalv  2274  equsal  2421  2sb6rf  2477  sbcom3  2510  moeu  2583  ralbiia  3080  ceqsal  3478  ceqsalv  3480  ceqsralv  3481  clel2g  3613  clel4g  3617  dfdif3OLD  4070  csbie2df  4395  rabeqsnd  4626  ralsng  4632  snssb  4739  frinxp  5707  idrefALT  6070  dfom2  7810  dfacacn  10052  kmlem8  10068  kmlem13  10073  kmlem14  10074  axgroth2  10736  bnj1171  35156  bnj1253  35173  orbi2iALT  35879  filnetlem4  36575  wl-equsalvw  37743  lcmineqlem4  42286  dvrelog2b  42320  aks6d1c1  42370  aks6d1c4  42378  aks6d1c6lem3  42426  elintima  43894  ichexmpl2  47716