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  1048  cador  1610  equsalvw  2006  ax13b  2034  sbbiiev  2098  equsalv  2275  equsal  2422  2sb6rf  2478  sbcom3  2511  moeu  2584  ralbiia  3082  ceqsal  3480  ceqsalv  3482  ceqsralv  3483  clel2g  3615  clel4g  3619  dfdif3OLD  4072  csbie2df  4397  rabeqsnd  4628  ralsng  4634  snssb  4741  frinxp  5715  idrefALT  6078  dfom2  7820  dfacacn  10064  kmlem8  10080  kmlem13  10085  kmlem14  10086  axgroth2  10748  bnj1171  35175  bnj1253  35192  orbi2iALT  35898  filnetlem4  36594  wl-equsalvw  37790  qmapeldisjsim  39108  lcmineqlem4  42399  dvrelog2b  42433  aks6d1c1  42483  aks6d1c4  42491  aks6d1c6lem3  42539  elintima  44006  ichexmpl2  47827