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  336  bibi2d  343  ibib  368  ibibr  369  pm5.4  390  pm5.42  544  anclb  546  ancrb  548  pm5.3  573  cases2  1045  cador  1610  equsalvw  2007  ax13b  2035  sbcom3vv  2098  equsalv  2259  equsal  2417  2sb6rf  2473  sbcom3  2510  moeu  2583  ralbiia  3091  ceqsalv  3467  ceqsralv  3469  clel2g  3588  clel4g  3593  elabg  3607  dfdif3  4049  csbie2df  4374  ralsng  4609  frinxp  5669  idrefALT  6018  dfom2  7714  dfacacn  9897  kmlem8  9913  kmlem13  9918  kmlem14  9919  axgroth2  10581  rabeqsnd  30848  bnj1171  32980  bnj1253  32997  filnetlem4  34570  wl-equsalvw  35697  lcmineqlem4  40040  dvrelog2b  40074  elintima  41261  ichexmpl2  44922