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  344  ibib  369  ibibr  370  pm5.4  390  pm5.42  544  anclb  546  ancrb  548  pm5.3  573  cases2  1040  cador  1590  equsalvw  1987  ax13b  2016  sbcom3vv  2073  equsalv  2231  equsal  2395  2sb6rf  2454  2sb6rfOLD  2455  sbcom3  2502  moeu  2628  ralbiia  3131  dfdif3  4012  frinxp  5520  idrefALT  5849  dfom2  7438  dfacacn  9413  kmlem8  9429  kmlem13  9434  kmlem14  9435  axgroth2  10093  rabeqsnd  29956  bnj1171  31886  bnj1253  31903  filnetlem4  33338  wl-equsalvw  34310  elintima  39483  ichexmpl2  43114