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  696  pm4.14dc  895  pm5.6dc  931  2sb6  2035  2sb6rf  2041  2exsb  2060  mor  2120  eu2  2122  moanim  2152  r2alf  2547  r3al  2574  r19.23t  2638  ceqsralt  2827  rspc2gv  2919  ralrab  2964  ralrab2  2968  euind  2990  reu2  2991  reu3  2993  rmo4  2996  rmo3f  3000  reuind  3008  rmo2ilem  3119  rmo3  3121  ralss  3290  rabss  3301  raldifb  3344  unissb  3917  elintrab  3934  ssintrab  3945  dftr5  4184  repizf2lem  4244  reusv3  4548  tfi  4671  raliunxp  4860  fununi  5385  dff13  5885  dfsmo2  6423  tfr1onlemaccex  6484  tfrcllemaccex  6497  qliftfun  6754  nnnninfeq2  7284  prime  9534  raluz  9761  raluz2  9762  ralrp  9859  facwordi  10949  modfsummod  11955  nnwosdc  12546  isprm2  12625  isprm4  12627  metcnp  15171  limcdifap  15321  bdcriota  16176  nnnninfex  16319