Theorem 3expa 1193

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 1192	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 254	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 968

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  df-3an 970

This theorem is referenced by:  ad4ant123  1205  ad4ant124  1206  ad4ant134  1207  ad4ant234  1208  3anidm23  1287  mp3an2  1315  mpd3an3  1328  rgen3  2553  moi2  2907  sbc3ie  3024  preq12bg  3753  issod  4297  wepo  4337  reuhypd  4449  funimass4  5537  fvtp1g  5693  f1imass  5742  fcof1o  5757  f1ofveu  5830  f1ocnvfv3  5831  acexmid  5841  2ndrn  6151  frecrdg  6376  oawordriexmid  6438  mapxpen  6814  findcard  6854  findcard2  6855  findcard2s  6856  ltapig  7279  ltanqi  7343  ltmnqi  7344  lt2addnq  7345  lt2mulnq  7346  prarloclemcalc  7443  genpassl  7465  genpassu  7466  prmuloc  7507  ltexprlemm  7541  ltexprlemfl  7550  ltexprlemfu  7552  lteupri  7558  ltaprg  7560  mul4  8030  add4  8059  cnegexlem2  8074  cnegexlem3  8075  2addsub  8112  addsubeq4  8113  muladd  8282  ltleadd  8344  reapmul1  8493  apreim  8501  receuap  8566  p1le  8744  lemul12b  8756  lbinf  8843  zdiv  9279  fzind  9306  fnn0ind  9307  uzss  9486  qmulcl  9575  qreccl  9580  xrlttr  9731  xaddass  9805  icc0r  9862  iooshf  9888  elfz5  9952  elfz0fzfz0  10061  fzind2  10174  ioo0  10195  ico0  10197  ioc0  10198  expnegap0  10463  expineg2  10464  mulexpzap  10495  expsubap  10503  expnbnd  10578  facndiv  10652  bccmpl  10667  bcval5  10676  bcpasc  10679  crim  10800  climshftlemg  11243  2sumeq2dv  11312  hash2iun  11420  2cprodeq2dv  11509  dvdsval3  11731  dvdsnegb  11748  muldvds1  11756  muldvds2  11757  dvdscmul  11758  dvdsmulc  11759  dvds2ln  11764  divalgb  11862  ndvdssub  11867  gcddiv  11952  rpexp1i  12086  phiprmpw  12154  hashgcdeq  12171  pythagtriplem1  12197  pockthg  12287  infpnlem1  12289  4sqlem3  12320  innei  12803  iscnp4  12858  cnpnei  12859  cnnei  12872  cnconst  12874  ismeti  12986  isxmet2d  12988  elbl2ps  13032  elbl2  13033  xblpnfps  13038  xblpnf  13039  xblm  13057  blininf  13064  blssexps  13069  blssex  13070  blsscls2  13133  metss  13134  metrest  13146  metcn  13154  divcnap  13195  cdivcncfap  13227  lgslem4  13544  lgscllem  13548  lgsneg1  13566  lgsne0  13579