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  2039  ax13b  2067  sbbiiev  2132  equsalv  2305  equsal  2449  2sb6rf  2505  sbcom3  2538  moeu  2611  ralbiia  3110  ceqsal  3491  ceqsalv  3493  ceqsralv  3494  clel2g  3616  clel4g  3620  csbie2df  4404  rabeqsnd  4631  ralsng  4637  snssb  4745  frinxp  5742  idrefALT  6125  dfom2  7913  dfacacn  10259  kmlem8  10275  kmlem13  10280  kmlem14  10281  axgroth2  10949  bnj1171  35741  bnj1253  35758  orbi2iALT  36658  filnetlem4  37384  mh-regprimbi  37548  mh-infprim1bi  37549  wl-equsalvw  38738  qmapeldisjsim  40058  lcmineqlem4  43348  dvrelog2b  43382  aks6d1c1  43432  aks6d1c4  43440  aks6d1c6lem3  43488  elintima  44914  ichexmpl2  48825