Theorem 3expa 1234

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ad4ant123  1246  ad4ant124  1247  ad4ant134  1248  ad4ant234  1249  ad5ant123  1270  3anidm23  1338  mp3an2  1366  mpd3an3  1379  rgen3  2637  moi2  3007  sbc3ie  3125  2if2dc  3680  preq12bg  3898  issod  4464  wepo  4504  reuhypd  4617  funimass4  5753  fvtp1g  5923  f1imass  5980  fcof1o  5995  f1ofveu  6073  f1ocnvfv3  6074  acexmid  6084  2ndrn  6417  funsssuppss  6498  frecrdg  6679  oawordriexmid  6743  mapxpen  7148  findcard  7192  findcard2  7193  findcard2s  7194  ltapig  7706  ltanqi  7770  ltmnqi  7771  lt2addnq  7772  lt2mulnq  7773  prarloclemcalc  7870  genpassl  7892  genpassu  7893  prmuloc  7934  ltexprlemm  7968  ltexprlemfl  7977  ltexprlemfu  7979  lteupri  7985  ltaprg  7987  mul4  8460  add4  8489  cnegexlem2  8504  cnegexlem3  8505  2addsub  8542  addsubeq4  8543  muladd  8713  ltleadd  8776  reapmul1  8926  apreim  8934  receuap  9002  p1le  9182  lemul12b  9194  lbinf  9281  zdiv  9739  fzind  9766  fnn0ind  9767  uzss  9953  qmulcl  10047  qreccl  10052  xrlttr  10208  xaddass  10282  icc0r  10339  iooshf  10365  elfz5  10431  elfz0fzfz0  10544  fzind2  10669  ioo0  10705  ico0  10707  ioc0  10708  expnegap0  10999  expineg2  11000  mulexpzap  11031  expsubap  11039  expnbnd  11116  facndiv  11193  bccmpl  11208  bcval5  11217  bcpasc  11220  ccatrn  11393  swrdspsleq  11455  swrdccat2  11459  ccatpfx  11489  pfxccat1  11490  swrdswrd  11493  cats1un  11509  crim  11639  climshftlemg  12087  2sumeq2dv  12156  hash2iun  12265  2cprodeq2dv  12354  dvdsval3  12577  dvdsnegb  12594  muldvds1  12602  muldvds2  12603  dvdscmul  12604  dvdsmulc  12605  dvds2ln  12610  divalgb  12711  ndvdssub  12716  gcddiv  12815  rpexp1i  12952  phiprmpw  13023  hashgcdeq  13041  pythagtriplem1  13067  pockthg  13159  infpnlem1  13161  4sqlem3  13192  imasaddfnlemg  13688  mndpfo  13804  grplmulf1o  13932  grplactcnv  13960  mulgnn0subcl  13991  mulgsubcl  13992  mulgdir  14010  issubg2m  14045  issubgrpd2  14046  nmzsubg  14066  eqgen  14083  ghmmulg  14112  ghmf1  14129  kerf1ghm  14130  conjghm  14132  srglmhm  14381  srgrmhm  14382  ringlghm  14450  ringrghm  14451  oppr1g  14472  dvdsrcl2  14490  crngunit  14502  subsubrng  14606  subrgugrp  14632  subsubrg  14637  islmod  14711  lmodvsdir  14733  lmodvsass  14734  lsssubg  14798  lss1d  14804  lidlsubg  14907  lidlsubcl  14908  expghmap  15026  mulgghm2  15027  innei  15355  iscnp4  15410  cnpnei  15411  cnnei  15424  cnconst  15426  ismeti  15538  isxmet2d  15540  elbl2ps  15584  elbl2  15585  xblpnfps  15590  xblpnf  15591  xblm  15609  blininf  15616  blssexps  15621  blssex  15622  blsscls2  15685  metss  15686  metrest  15698  metcn  15706  divcnap  15757  cdivcncfap  15796  dvply1  15957  logdivlt  16088  lgslem4  16288  lgscllem  16292  lgsneg1  16310  lgsne0  16323  uspgr2wlkeq  16772  eupth2lem3lem7fi  16881