Theorem pm5.74i 274

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bitrd  282  imbi2i  339  bibi2d  345  ibib  370  ibibr  371  pm5.4  392  pm5.42  552  anclb  554  ancrb  556  pm5.3  582  cases2  1061  cador  1635  equsalvw  2031  ax13b  2059  sbbiiev  2133  equsalv  2309  equsal  2455  2sb6rf  2511  sbcom3  2544  moeu  2617  ralbiia  3115  ceqsal  3500  ceqsalv  3502  ceqsralv  3503  clel2g  3627  clel4g  3631  dfdif3OLD  4081  csbie2df  4406  rabeqsnd  4637  ralsng  4643  snssb  4750  frinxp  5742  idrefALT  6111  dfom2  7860  dfacacn  10121  kmlem8  10137  kmlem13  10142  kmlem14  10143  axgroth2  10806  bnj1171  35329  bnj1253  35346  orbi2iALT  36072  filnetlem4  36777  mh-regprimbi  36941  mh-infprim1bi  36942  wl-equsalvw  38076  qmapeldisjsim  39394  lcmineqlem4  42684  dvrelog2b  42718  aks6d1c1  42768  aks6d1c4  42776  aks6d1c6lem3  42824  elintima  44266  ichexmpl2  48103