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  346  ibib  371  ibibr  372  pm5.4  393  pm5.42  547  anclb  549  ancrb  551  pm5.3  576  cases2  1048  cador  1615  equsalvw  2012  ax13b  2040  sbcom3vv  2102  equsalv  2264  equsal  2416  2sb6rf  2472  sbcom3  2509  moeu  2582  ralbiia  3087  ceqsalv  3443  ceqsralv  3445  clel2g  3566  clel4g  3571  elabg  3585  dfdif3  4029  csbie2df  4355  ralsng  4589  frinxp  5631  idrefALT  5978  dfom2  7646  dfacacn  9755  kmlem8  9771  kmlem13  9776  kmlem14  9777  axgroth2  10439  rabeqsnd  30567  bnj1171  32693  bnj1253  32710  filnetlem4  34307  wl-equsalvw  35434  lcmineqlem4  39774  dvrelog2b  39807  elintima  40938  ichexmpl2  44595