Theorem pm5.74i 259

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 258	. 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)))
3	1, 2	mpbi 219	1 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  bitrd  267  imbi2i  325  bibi2d  331  ibib  356  ibibr  357  anclb  568  pm5.42  569  ancrb  571  cador  1538  equsalvw  1918  ax13b  1951  equsalhw  2109  equsal  2279  sbcom3  2399  2sb6rf  2440  ralbiia  2962  frinxp  5107  dfom2  6959  dfacacn  8846  kmlem8  8862  kmlem13  8867  kmlem14  8868  axgroth2  9526  bnj1171  30322  bnj1253  30339  filnetlem4  31546  bj-ssb1a  31821  bj-ssb1  31822  bj-ssbcom3lem  31839  bj-equsalv  31931  wl-sbcom3  32551  elintima  36964