Theorem pm5.74i 272

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  bitrd  280  imbi2i  337  bibi2d  343  ibib  368  ibibr  369  pm5.4  389  pm5.42  548  anclb  550  ancrb  552  pm5.3  577  cases2  1053  cador  1615  equsalvw  2011  ax13b  2039  sbbiiev  2103  equsalv  2279  equsal  2425  2sb6rf  2481  sbcom3  2514  moeu  2587  ralbiia  3083  ceqsal  3468  ceqsalv  3470  ceqsralv  3471  clel2g  3597  clel4g  3601  dfdif3OLD  4049  csbie2df  4371  rabeqsnd  4601  ralsng  4607  snssb  4714  frinxp  5701  idrefALT  6063  dfom2  7808  dfacacn  10055  kmlem8  10071  kmlem13  10076  kmlem14  10077  axgroth2  10739  bnj1171  35182  bnj1253  35199  orbi2iALT  35913  filnetlem4  36609  mh-regprimbi  36773  mh-infprim1bi  36774  wl-equsalvw  37909  qmapeldisjsim  39227  lcmineqlem4  42517  dvrelog2b  42551  aks6d1c1  42601  aks6d1c4  42609  aks6d1c6lem3  42657  elintima  44097  ichexmpl2  47945