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  1063  cador  1638  equsalvw  2034  ax13b  2062  sbbiiev  2127  equsalv  2303  equsal  2449  2sb6rf  2505  sbcom3  2538  moeu  2611  ralbiia  3109  ceqsal  3492  ceqsalv  3494  ceqsralv  3495  clel2g  3618  clel4g  3622  dfdif3OLD  4073  csbie2df  4408  rabeqsnd  4635  ralsng  4641  snssb  4748  frinxp  5744  idrefALT  6113  dfom2  7860  dfacacn  10121  kmlem8  10137  kmlem13  10142  kmlem14  10143  axgroth2  10805  bnj1171  35388  bnj1253  35405  orbi2iALT  36177  filnetlem4  36892  mh-regprimbi  37056  mh-infprim1bi  37057  wl-equsalvw  38193  qmapeldisjsim  39509  lcmineqlem4  42799  dvrelog2b  42833  aks6d1c1  42883  aks6d1c4  42891  aks6d1c6lem3  42939  elintima  44379  ichexmpl2  48219