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  346  exp4a  363  imdistan  440  pm5.3  466  pm4.87  546  nan  681  pm4.14dc  875  pm5.6dc  911  2sb6  1959  2sb6rf  1965  2exsb  1984  mor  2041  eu2  2043  moanim  2073  r2alf  2452  r3al  2477  r19.23t  2539  ceqsralt  2713  rspc2gv  2801  ralrab  2845  ralrab2  2849  euind  2871  reu2  2872  reu3  2874  rmo4  2877  rmo3f  2881  reuind  2889  rmo2ilem  2998  rmo3  3000  ralss  3163  rabss  3174  raldifb  3216  unissb  3766  elintrab  3783  ssintrab  3794  dftr5  4029  repizf2lem  4085  reusv3  4381  tfi  4496  raliunxp  4680  fununi  5191  dff13  5669  dfsmo2  6184  tfr1onlemaccex  6245  tfrcllemaccex  6258  qliftfun  6511  prime  9150  raluz  9373  raluz2  9374  ralrp  9463  facwordi  10486  modfsummod  11227  isprm2  11798  isprm4  11800  metcnp  12681  limcdifap  12800  bdcriota  13081