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  699  pm4.14dc  898  pm5.6dc  934  2sb6  2037  2sb6rf  2043  2exsb  2062  mor  2122  eu2  2124  moanim  2154  r2alf  2550  r3al  2577  r19.23t  2641  ceqsralt  2831  rspc2gv  2923  ralrab  2968  ralrab2  2972  euind  2994  reu2  2995  reu3  2997  rmo4  3000  rmo3f  3004  reuind  3012  rmo2ilem  3123  rmo3  3125  ralss  3294  rabss  3305  raldifb  3349  unissb  3928  elintrab  3945  ssintrab  3956  dftr5  4195  repizf2lem  4257  reusv3  4563  tfi  4686  raliunxp  4877  fununi  5405  dff13  5919  dfsmo2  6496  tfr1onlemaccex  6557  tfrcllemaccex  6570  qliftfun  6829  nnnninfeq2  7371  prime  9622  raluz  9855  raluz2  9856  ralrp  9953  facwordi  11046  modfsummod  12080  nnwosdc  12671  isprm2  12750  isprm4  12752  metcnp  15303  limcdifap  15453  bdcriota  16579  nnnninfex  16728