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  3249  rabss  3260  raldifb  3303  unissb  3869  elintrab  3886  ssintrab  3897  dftr5  4134  repizf2lem  4194  reusv3  4495  tfi  4618  raliunxp  4807  fununi  5326  dff13  5815  dfsmo2  6345  tfr1onlemaccex  6406  tfrcllemaccex  6419  qliftfun  6676  nnnninfeq2  7195  prime  9425  raluz  9652  raluz2  9653  ralrp  9750  facwordi  10832  modfsummod  11623  nnwosdc  12206  isprm2  12285  isprm4  12287  metcnp  14748  limcdifap  14898  bdcriota  15529