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 230	1 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bitrd  279  imbi2i  336  bibi2d  342  ibib  367  ibibr  368  pm5.4  388  pm5.42  543  anclb  545  ancrb  547  pm5.3  572  cases2  1047  cador  1605  equsalvw  2001  ax13b  2029  sbbiiev  2090  equsalv  2265  equsal  2420  2sb6rf  2476  sbcom3  2509  moeu  2581  ralbiia  3089  ceqsal  3517  ceqsalv  3519  ceqsralv  3520  clel2g  3659  clel4g  3663  elabg  3677  dfdif3OLD  4128  csbie2df  4449  rabeqsnd  4674  ralsng  4680  snssb  4787  frinxp  5771  idrefALT  6134  dfom2  7889  dfacacn  10180  kmlem8  10196  kmlem13  10201  kmlem14  10202  axgroth2  10863  bnj1171  34993  bnj1253  35010  orbi2iALT  35670  filnetlem4  36364  wl-equsalvw  37519  lcmineqlem4  42014  dvrelog2b  42048  aks6d1c1  42098  aks6d1c4  42106  aks6d1c6lem3  42154  elintima  43643  ichexmpl2  47395