Theorem impexp 263

Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)

Assertion

Ref	Expression
impexp	⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

Proof of Theorem impexp

Step	Hyp	Ref	Expression
1		pm3.3 261	. 2 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
2		pm3.31 262	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒))
3	1, 2	impbii 126	1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imp4a  349  exp4a  366  imdistan  444  pm5.3  475  pm4.87  557  nan  693  pm4.14dc  891  pm5.6dc  927  2sb6  2003  2sb6rf  2009  2exsb  2028  mor  2087  eu2  2089  moanim  2119  r2alf  2514  r3al  2541  r19.23t  2604  ceqsralt  2790  rspc2gv  2880  ralrab  2925  ralrab2  2929  euind  2951  reu2  2952  reu3  2954  rmo4  2957  rmo3f  2961  reuind  2969  rmo2ilem  3079  rmo3  3081  ralss  3250  rabss  3261  raldifb  3304  unissb  3870  elintrab  3887  ssintrab  3898  dftr5  4135  repizf2lem  4195  reusv3  4496  tfi  4619  raliunxp  4808  fununi  5327  dff13  5818  dfsmo2  6354  tfr1onlemaccex  6415  tfrcllemaccex  6428  qliftfun  6685  nnnninfeq2  7204  prime  9444  raluz  9671  raluz2  9672  ralrp  9769  facwordi  10851  modfsummod  11642  nnwosdc  12233  isprm2  12312  isprm4  12314  metcnp  14856  limcdifap  15006  bdcriota  15637  nnnninfex  15777