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  9442  raluz  9669  raluz2  9670  ralrp  9767  facwordi  10849  modfsummod  11640  nnwosdc  12231  isprm2  12310  isprm4  12312  metcnp  14832  limcdifap  14982  bdcriota  15613