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  694  pm4.14dc  892  pm5.6dc  928  2sb6  2013  2sb6rf  2019  2exsb  2038  mor  2097  eu2  2099  moanim  2129  r2alf  2524  r3al  2551  r19.23t  2614  ceqsralt  2801  rspc2gv  2891  ralrab  2936  ralrab2  2940  euind  2962  reu2  2963  reu3  2965  rmo4  2968  rmo3f  2972  reuind  2980  rmo2ilem  3090  rmo3  3092  ralss  3261  rabss  3272  raldifb  3315  unissb  3883  elintrab  3900  ssintrab  3911  dftr5  4150  repizf2lem  4210  reusv3  4512  tfi  4635  raliunxp  4824  fununi  5348  dff13  5847  dfsmo2  6383  tfr1onlemaccex  6444  tfrcllemaccex  6457  qliftfun  6714  nnnninfeq2  7243  prime  9485  raluz  9712  raluz2  9713  ralrp  9810  facwordi  10898  modfsummod  11819  nnwosdc  12410  isprm2  12489  isprm4  12491  metcnp  15034  limcdifap  15184  bdcriota  15933  nnnninfex  16074