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 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  279  imbi2i  336  bibi2d  343  ibib  368  ibibr  369  pm5.4  390  pm5.42  545  anclb  547  ancrb  549  pm5.3  574  cases2  1047  cador  1610  equsalvw  2008  ax13b  2036  sbcom3vv  2099  equsalv  2259  equsal  2417  2sb6rf  2473  sbcom3  2506  moeu  2578  ralbiia  3092  ceqsal  3510  ceqsalv  3512  ceqsralv  3514  clel2g  3648  clel4g  3653  elabg  3667  dfdif3  4115  csbie2df  4441  rabeqsnd  4672  ralsng  4678  snssb  4787  frinxp  5759  idrefALT  6113  dfom2  7857  dfacacn  10136  kmlem8  10152  kmlem13  10157  kmlem14  10158  axgroth2  10820  bnj1171  34011  bnj1253  34028  filnetlem4  35266  wl-equsalvw  36407  lcmineqlem4  40897  dvrelog2b  40931  elintima  42404  ichexmpl2  46138