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  4245  reusv3  4551  tfi  4674  raliunxp  4863  fununi  5389  dff13  5892  dfsmo2  6433  tfr1onlemaccex  6494  tfrcllemaccex  6507  qliftfun  6764  nnnninfeq2  7296  prime  9546  raluz  9773  raluz2  9774  ralrp  9871  facwordi  10962  modfsummod  11969  nnwosdc  12560  isprm2  12639  isprm4  12641  metcnp  15186  limcdifap  15336  bdcriota  16246  nnnninfex  16388