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 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  imp4a  349  exp4a  366  imdistan  448  pm5.3  479  pm4.87  563  nan  703  pm4.14dc  902  pm5.6dc  938  2sb6  2044  2sb6rf  2050  2exsb  2069  mor  2129  eu2  2131  moanim  2161  r2alf  2567  r3al  2594  r19.23t  2658  ceqsralt  2849  rspc2gv  2942  ralrab  2987  ralrab2  2991  euind  3013  reu2  3014  reu3  3016  rmo4  3019  rmo3f  3023  reuind  3031  rmo2ilem  3142  rmo3  3144  ralss  3314  rabss  3325  raldifb  3369  unissb  3965  elintrab  3982  ssintrab  3993  dftr5  4234  repizf2lem  4300  reusv3  4608  tfi  4731  raliunxp  4923  fununi  5452  dff13  5977  dfsmo2  6562  tfr1onlemaccex  6623  tfrcllemaccex  6636  qliftfun  6895  nnnninfeq2  7476  prime  9757  raluz  9995  raluz2  9996  ralrp  10094  facwordi  11201  modfsummod  12251  nnwosdc  12842  isprm2  12921  isprm4  12923  metcnp  15750  limcdifap  15900  bdcriota  17126  nnnninfex  17283  dfrals2  17349  dfralseu2  17383