Theorem pm5.74i 274

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bitrd  282  imbi2i  339  bibi2d  345  ibib  370  ibibr  371  pm5.4  393  pm5.42  553  anclb  555  ancrb  557  pm5.3  583  cases2  1063  cador  1641  equsalvw  2037  ax13b  2065  sbbiiev  2130  equsalv  2302  equsal  2447  2sb6rf  2503  sbcom3  2536  moeu  2609  ralbiia  3107  ceqsal  3488  ceqsalv  3490  ceqsralv  3491  clel2g  3613  clel4g  3617  csbie2df  4401  rabeqsnd  4630  ralsng  4636  snssb  4743  frinxp  5734  idrefALT  6107  dfom2  7877  dfacacn  10213  kmlem8  10229  kmlem13  10234  kmlem14  10235  axgroth2  10903  bnj1171  35623  bnj1253  35640  orbi2iALT  36429  filnetlem4  37149  mh-regprimbi  37313  mh-infprim1bi  37314  wl-equsalvw  38450  qmapeldisjsim  39772  lcmineqlem4  43062  dvrelog2b  43096  aks6d1c1  43146  aks6d1c4  43154  aks6d1c6lem3  43202  elintima  44638  ichexmpl2  48521