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  342  ibib  367  ibibr  368  pm5.4  389  pm5.42  544  anclb  546  ancrb  548  pm5.3  573  cases2  1046  cador  1609  equsalvw  2007  ax13b  2035  sbcom3vv  2098  equsalv  2258  equsal  2415  2sb6rf  2471  sbcom3  2504  moeu  2576  ralbiia  3090  ceqsal  3507  ceqsalv  3509  ceqsralv  3511  clel2g  3643  clel4g  3648  elabg  3662  dfdif3  4110  csbie2df  4436  ralsng  4670  snssb  4779  frinxp  5750  idrefALT  6101  dfom2  7840  dfacacn  10118  kmlem8  10134  kmlem13  10139  kmlem14  10140  axgroth2  10802  rabeqsnd  31604  bnj1171  33842  bnj1253  33859  filnetlem4  35070  wl-equsalvw  36211  lcmineqlem4  40702  dvrelog2b  40736  elintima  42175  ichexmpl2  45910