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  696  pm4.14dc  895  pm5.6dc  931  2sb6  2035  2sb6rf  2041  2exsb  2060  mor  2120  eu2  2122  moanim  2152  r2alf  2547  r3al  2574  r19.23t  2638  ceqsralt  2828  rspc2gv  2920  ralrab  2965  ralrab2  2969  euind  2991  reu2  2992  reu3  2994  rmo4  2997  rmo3f  3001  reuind  3009  rmo2ilem  3120  rmo3  3122  ralss  3291  rabss  3302  raldifb  3345  unissb  3921  elintrab  3938  ssintrab  3949  dftr5  4188  repizf2lem  4249  reusv3  4555  tfi  4678  raliunxp  4869  fununi  5395  dff13  5904  dfsmo2  6448  tfr1onlemaccex  6509  tfrcllemaccex  6522  qliftfun  6781  nnnninfeq2  7322  prime  9572  raluz  9805  raluz2  9806  ralrp  9903  facwordi  10995  modfsummod  12012  nnwosdc  12603  isprm2  12682  isprm4  12684  metcnp  15229  limcdifap  15379  bdcriota  16428  nnnninfex  16574