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  698  pm4.14dc  897  pm5.6dc  933  2sb6  2037  2sb6rf  2043  2exsb  2062  mor  2122  eu2  2124  moanim  2154  r2alf  2549  r3al  2576  r19.23t  2640  ceqsralt  2830  rspc2gv  2922  ralrab  2967  ralrab2  2971  euind  2993  reu2  2994  reu3  2996  rmo4  2999  rmo3f  3003  reuind  3011  rmo2ilem  3122  rmo3  3124  ralss  3293  rabss  3304  raldifb  3347  unissb  3923  elintrab  3940  ssintrab  3951  dftr5  4190  repizf2lem  4251  reusv3  4557  tfi  4680  raliunxp  4871  fununi  5398  dff13  5909  dfsmo2  6453  tfr1onlemaccex  6514  tfrcllemaccex  6527  qliftfun  6786  nnnninfeq2  7328  prime  9579  raluz  9812  raluz2  9813  ralrp  9910  facwordi  11003  modfsummod  12024  nnwosdc  12615  isprm2  12694  isprm4  12696  metcnp  15242  limcdifap  15392  bdcriota  16504  nnnninfex  16650