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  347  exp4a  364  imdistan  441  pm5.3  467  pm4.87  547  nan  682  pm4.14dc  876  pm5.6dc  912  2sb6  1960  2sb6rf  1966  2exsb  1985  mor  2042  eu2  2044  moanim  2074  r2alf  2455  r3al  2480  r19.23t  2542  ceqsralt  2716  rspc2gv  2805  ralrab  2849  ralrab2  2853  euind  2875  reu2  2876  reu3  2878  rmo4  2881  rmo3f  2885  reuind  2893  rmo2ilem  3002  rmo3  3004  ralss  3168  rabss  3179  raldifb  3221  unissb  3774  elintrab  3791  ssintrab  3802  dftr5  4037  repizf2lem  4093  reusv3  4389  tfi  4504  raliunxp  4688  fununi  5199  dff13  5677  dfsmo2  6192  tfr1onlemaccex  6253  tfrcllemaccex  6266  qliftfun  6519  prime  9174  raluz  9400  raluz2  9401  ralrp  9492  facwordi  10518  modfsummod  11259  isprm2  11834  isprm4  11836  metcnp  12720  limcdifap  12839  bdcriota  13252