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  2416  2sb6rf  2472  sbcom3  2505  moeu  2577  ralbiia  3091  ceqsal  3509  ceqsalv  3511  ceqsralv  3513  clel2g  3646  clel4g  3651  elabg  3665  dfdif3  4113  csbie2df  4439  rabeqsnd  4670  ralsng  4676  snssb  4785  frinxp  5756  idrefALT  6109  dfom2  7853  dfacacn  10132  kmlem8  10148  kmlem13  10153  kmlem14  10154  axgroth2  10816  bnj1171  33999  bnj1253  34016  filnetlem4  35254  wl-equsalvw  36395  lcmineqlem4  40885  dvrelog2b  40919  elintima  42389  ichexmpl2  46124