Theorem impexp 261

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 259	. 2 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
2		pm3.31 260	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒))
3	1, 2	impbii 125	1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imp4a  347  exp4a  364  imdistan  441  pm5.3  467  pm4.87  547  nan  682  pm4.14dc  876  pm5.6dc  912  2sb6  1964  2sb6rf  1970  2exsb  1989  mor  2048  eu2  2050  moanim  2080  r2alf  2474  r3al  2501  r19.23t  2564  ceqsralt  2739  rspc2gv  2828  ralrab  2873  ralrab2  2877  euind  2899  reu2  2900  reu3  2902  rmo4  2905  rmo3f  2909  reuind  2917  rmo2ilem  3026  rmo3  3028  ralss  3194  rabss  3205  raldifb  3247  unissb  3802  elintrab  3819  ssintrab  3830  dftr5  4065  repizf2lem  4121  reusv3  4418  tfi  4539  raliunxp  4724  fununi  5235  dff13  5713  dfsmo2  6228  tfr1onlemaccex  6289  tfrcllemaccex  6302  qliftfun  6555  prime  9246  raluz  9472  raluz2  9473  ralrp  9564  facwordi  10596  modfsummod  11337  isprm2  11974  isprm4  11976  metcnp  12872  limcdifap  12991  bdcriota  13417