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  2038  2sb6rf  2044  2exsb  2063  mor  2123  eu2  2125  moanim  2155  r2alf  2559  r3al  2586  r19.23t  2650  ceqsralt  2840  rspc2gv  2932  ralrab  2977  ralrab2  2981  euind  3003  reu2  3004  reu3  3006  rmo4  3009  rmo3f  3013  reuind  3021  rmo2ilem  3132  rmo3  3134  ralss  3303  rabss  3314  raldifb  3358  unissb  3943  elintrab  3960  ssintrab  3971  dftr5  4210  repizf2lem  4273  reusv3  4580  tfi  4703  raliunxp  4895  fununi  5423  dff13  5940  dfsmo2  6517  tfr1onlemaccex  6578  tfrcllemaccex  6591  qliftfun  6850  nnnninfeq2  7419  prime  9676  raluz  9909  raluz2  9910  ralrp  10007  facwordi  11101  modfsummod  12140  nnwosdc  12731  isprm2  12810  isprm4  12812  metcnp  15369  limcdifap  15519  bdcriota  16645  nnnninfex  16792