Theorem pm5.74i 260

Description: Distribution of implication over biconditional (inference rule). (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 259	. 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)))
3	1, 2	mpbi 220	1 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  bitrd  268  imbi2i  325  bibi2d  331  ibib  356  ibibr  357  anclb  571  pm5.42  572  ancrb  574  cases2  1034  cador  1696  equsalvw  2086  ax13b  2115  equsalv  2255  equsalhw  2270  equsal  2436  sbcom3  2548  2sb6rf  2589  ralbiia  3117  dfdif3  3863  frinxp  5341  dfom2  7232  dfacacn  9155  kmlem8  9171  kmlem13  9176  kmlem14  9177  axgroth2  9839  rabeqsnd  29649  bnj1171  31375  bnj1253  31392  filnetlem4  32682  bj-ssb1a  32938  bj-ssb1  32939  bj-ssbcom3lem  32956  wl-sbcom3  33685  elintima  38447