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  692  pm4.14dc  890  pm5.6dc  926  2sb6  1984  2sb6rf  1990  2exsb  2009  mor  2068  eu2  2070  moanim  2100  r2alf  2494  r3al  2521  r19.23t  2584  ceqsralt  2766  rspc2gv  2855  ralrab  2900  ralrab2  2904  euind  2926  reu2  2927  reu3  2929  rmo4  2932  rmo3f  2936  reuind  2944  rmo2ilem  3054  rmo3  3056  ralss  3223  rabss  3234  raldifb  3277  unissb  3841  elintrab  3858  ssintrab  3869  dftr5  4106  repizf2lem  4163  reusv3  4462  tfi  4583  raliunxp  4770  fununi  5286  dff13  5771  dfsmo2  6290  tfr1onlemaccex  6351  tfrcllemaccex  6364  qliftfun  6619  nnnninfeq2  7129  prime  9354  raluz  9580  raluz2  9581  ralrp  9677  facwordi  10722  modfsummod  11468  nnwosdc  12042  isprm2  12119  isprm4  12121  metcnp  14051  limcdifap  14170  bdcriota  14674