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  5898  dfsmo2  6439  tfr1onlemaccex  6500  tfrcllemaccex  6513  qliftfun  6772  nnnninfeq2  7304  prime  9554  raluz  9781  raluz2  9782  ralrp  9879  facwordi  10970  modfsummod  11977  nnwosdc  12568  isprm2  12647  isprm4  12649  metcnp  15194  limcdifap  15344  bdcriota  16270  nnnninfex  16418