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 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  imp4a  349  exp4a  366  imdistan  448  pm5.3  479  pm4.87  563  nan  703  pm4.14dc  902  pm5.6dc  938  2sb6  2044  2sb6rf  2050  2exsb  2069  mor  2129  eu2  2131  moanim  2161  r2alf  2567  r3al  2594  r19.23t  2658  ceqsralt  2849  rspc2gv  2942  ralrab  2987  ralrab2  2991  euind  3013  reu2  3014  reu3  3016  rmo4  3019  rmo3f  3023  reuind  3031  rmo2ilem  3142  rmo3  3144  ralss  3314  rabss  3325  raldifb  3369  unissb  3965  elintrab  3982  ssintrab  3993  dftr5  4232  repizf2lem  4298  reusv3  4606  tfi  4729  raliunxp  4921  fununi  5449  dff13  5974  dfsmo2  6558  tfr1onlemaccex  6619  tfrcllemaccex  6632  qliftfun  6891  nnnninfeq2  7470  prime  9750  raluz  9988  raluz2  9989  ralrp  10087  facwordi  11193  modfsummod  12243  nnwosdc  12834  isprm2  12913  isprm4  12915  metcnp  15665  limcdifap  15815  bdcriota  17031  nnnninfex  17187  dfrals2  17252  dfralseu2  17286