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  2827  rspc2gv  2919  ralrab  2964  ralrab2  2968  euind  2990  reu2  2991  reu3  2993  rmo4  2996  rmo3f  3000  reuind  3008  rmo2ilem  3119  rmo3  3121  ralss  3290  rabss  3301  raldifb  3344  unissb  3918  elintrab  3935  ssintrab  3946  dftr5  4185  repizf2lem  4246  reusv3  4552  tfi  4675  raliunxp  4866  fununi  5392  dff13  5901  dfsmo2  6444  tfr1onlemaccex  6505  tfrcllemaccex  6518  qliftfun  6777  nnnninfeq2  7312  prime  9562  raluz  9790  raluz2  9791  ralrp  9888  facwordi  10979  modfsummod  11990  nnwosdc  12581  isprm2  12660  isprm4  12662  metcnp  15207  limcdifap  15357  bdcriota  16355  nnnninfex  16502