Theorem impexp 259

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  imp4a  341  exp4a  358  imdistan  432  pm5.3  458  pm4.87  523  nan  658  pm4.14dc  820  pm5.6dc  868  2sb6  1901  2sb6rf  1907  2exsb  1926  mor  1983  eu2  1985  moanim  2015  r2alf  2383  r3al  2408  r19.23t  2467  ceqsralt  2626  rspc2gv  2712  ralrab  2753  ralrab2  2757  euind  2779  reu2  2780  reu3  2782  rmo4  2785  reuind  2795  rmo2ilem  2903  rmo3  2905  ralss  3060  rabss  3071  raldifb  3112  unissb  3631  elintrab  3648  ssintrab  3659  dftr5  3878  repizf2lem  3935  reusv3  4210  tfi  4323  raliunxp  4495  fununi  4987  dff13  5428  dfsmo2  5925  qliftfun  6211  prime  8446  raluz  8666  raluz2  8667  ralrp  8755  facwordi  9667  isprm2  10499  isprm4  10501  bdcriota  10674