Theorem 3expa 1103

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((φ ∧ ψ ∧ χ) → θ)

Assertion

Ref	Expression
3expa	⊢ (((φ ∧ ψ) ∧ χ) → θ)

Proof of Theorem 3expa

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((φ ∧ ψ ∧ χ) → θ)
2	1	3exp 1102	. 2 ⊢ (φ → (ψ → (χ → θ)))
3	2	imp31 243	1 ⊢ (((φ ∧ ψ) ∧ χ) → θ)

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 884

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 886

This theorem is referenced by:  3anidm23  1193  mp3an2  1219  mpd3an3  1232  rgen3  2400  moi2  2716  sbc3ie  2825  preq12bg  3535  issod  4047  reuhypd  4169  funimass4  5167  fvtp1g  5312  f1imass  5356  fcof1o  5372  f1ofveu  5443  f1ocnvfv3  5444  acexmid  5454  2ndrn  5751  rdgon  5913  frecrdg  5931  ltapig  6322  ltanqi  6386  ltmnqi  6387  lt2addnq  6388  prarloclemcalc  6484  genpassl  6506  genpassu  6507  prmuloc  6546  ltexprlemm  6573  ltexprlemfl  6582  ltexprlemfu  6584  ltaprg  6591  mul4  6922  add4  6949  cnegexlem2  6964  cnegexlem3  6965  2addsub  7002  addsubeq4  7003  muladd  7157  ltleadd  7216  reapmul1  7359  apreim  7367  receuap  7412  p1le  7576  lemul12b  7588  zdiv  8084  fzind  8109  fnn0ind  8110  uzss  8249  qmulcl  8328  qreccl  8331  xrlttr  8466  icc0r  8545  iooshf  8571  elfz5  8632  elfz0fzfz0  8733  fzind2  8845  expnegap0  8897  expineg2  8898  mulexpzap  8929  expsubap  8936  expnbnd  9005  crim  9066