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  559  nan  699  pm4.14dc  898  pm5.6dc  934  2sb6  2040  2sb6rf  2046  2exsb  2065  mor  2125  eu2  2127  moanim  2157  r2alf  2561  r3al  2588  r19.23t  2652  ceqsralt  2843  rspc2gv  2936  ralrab  2981  ralrab2  2985  euind  3007  reu2  3008  reu3  3010  rmo4  3013  rmo3f  3017  reuind  3025  rmo2ilem  3136  rmo3  3138  ralss  3308  rabss  3319  raldifb  3363  unissb  3949  elintrab  3966  ssintrab  3977  dftr5  4216  repizf2lem  4279  reusv3  4586  tfi  4709  raliunxp  4901  fununi  5429  dff13  5947  dfsmo2  6531  tfr1onlemaccex  6592  tfrcllemaccex  6605  qliftfun  6864  nnnninfeq2  7433  prime  9695  raluz  9928  raluz2  9929  ralrp  10026  facwordi  11127  modfsummod  12169  nnwosdc  12760  isprm2  12839  isprm4  12841  metcnp  15489  limcdifap  15639  bdcriota  16765  nnnninfex  16912