Theorem 3impb 1114

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

Hypothesis

Ref	Expression
3impb.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
3impb	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impb

Step	Hyp	Ref	Expression
1		3impb.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	exp32 420	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1110	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1088

This theorem is referenced by:  3adant3  1131  3impdi  1349  rsp2e  3274  vtocl3gf  3562  vtocl3g  3564  rspc2ev  3624  reuss  4316  frc  5642  trssord  6381  funtp  6605  resdif  6854  f1cdmsn  7283  f1ofvswap  7307  fnotovb  7462  fovcdm  7581  fnovrn  7586  fmpoco  8086  smoord  8371  odi  8585  oeoa  8603  oeoe  8605  nndi  8629  ecopovtrn  8820  ecovass  8824  ecovdi  8825  unfi  9178  entrfil  9194  domtrfil  9201  f1imaenfi  9204  suppr  9472  infpr  9504  harval2  9998  fin23lem31  10344  tskuni  10784  addasspi  10896  mulasspi  10898  distrpi  10899  mulcanenq  10961  genpass  11010  distrlem1pr  11026  prlem934  11034  ltapr  11046  le2tri3i  11351  subadd  11470  addsub  11478  subdi  11654  submul2  11661  ltaddsub  11695  leaddsub  11697  divval  11881  div12  11901  diveq1  11912  divneg  11913  divdiv2  11933  ltmulgt11  12081  gt0div  12087  ge0div  12088  uzind3  12663  fnn0ind  12668  qdivcl  12961  irrmul  12965  xrlttr  13126  fzen  13525  modcyc  13878  modcyc2  13879  rpexpmord  14140  faclbnd4lem4  14263  ccatval21sw  14542  lswccatn0lsw  14548  ccatpfx  14658  ccatopth  14673  cshweqdifid  14777  lenegsq  15274  moddvds  16215  dvdscmulr  16235  dvdsmulcr  16236  dvds2add  16240  dvds2sub  16241  dvdsleabs  16261  divalg  16353  divalgb  16354  ndvdsadd  16360  gcdcllem3  16449  dvdslegcd  16452  modgcd  16481  absmulgcd  16498  odzval  16731  pcmul  16791  ressid2  17184  ressval2  17185  catcisolem  18070  prf1st  18166  prf2nd  18167  1st2ndprf  18168  curfuncf  18201  curf2ndf  18210  pltval  18295  pospo  18308  lubel  18477  isdlat  18485  submgmcl  18638  prdssgrpd  18664  issubmnd  18692  prdsmndd  18698  submcl  18735  grpinvid1  18919  grpinvid2  18920  mulgp1  19030  ghmlin  19142  ghmsub  19145  odlem2  19455  gexlem2  19498  lsmvalx  19555  efgtval  19639  cmncom  19714  lssvnegcl  20799  islss3  20802  prdslmodd  20812  zntoslem  21422  evlslem2  21953  evlseu  21957  maducoeval2  22462  madutpos  22464  madugsum  22465  madurid  22466  m2cpminvid  22575  pm2mpghm  22638  unopn  22725  ntrss  22879  innei  22949  t1sep2  23193  metustsym  24384  cncfi  24734  rrxds  25241  quotval  26144  abelthlem2  26284  mudivsum  27376  padicabv  27476  nosupfv  27552  nosupres  27553  noinffv  27567  ssltsepc  27639  divsval  28002  axsegconlem1  28608  nsnlplig  30167  nsnlpligALT  30168  grpoinvid1  30214  grpoinvid2  30215  grpodivval  30221  ablo4  30236  ablonncan  30242  nvnpcan  30342  nvmeq0  30344  nvabs  30358  imsdval  30372  ipval  30389  nmorepnf  30454  blo3i  30488  blometi  30489  ipasslem5  30521  hvmulcan  30758  his5  30772  his7  30776  his2sub2  30779  hhssabloilem  30947  hhssnv  30950  fh1  31304  fh2  31305  cm2j  31306  homcl  31432  homco1  31487  homulass  31488  hoadddi  31489  hosubsub2  31498  braadd  31631  bramul  31632  lnopmul  31653  lnopli  31654  lnopaddmuli  31659  lnopsubmuli  31661  lnfnli  31726  lnfnaddmuli  31731  kbass2  31803  mdexchi  32021  xdivval  32518  resvid2  32878  resvval2  32879  fedgmullem2  33169  unitdivcld  33345  bnj229  34359  bnj546  34371  bnj570  34380  cusgredgex2  34577  loop1cycl  34592  cvmlift2lem7  34764  finminlem  35667  ivthALT  35684  topdifinffinlem  36692  lindsadd  36945  exidcl  37208  grposnOLD  37214  rngoneglmul  37275  rngonegrmul  37276  divrngcl  37289  crngocom  37333  crngm4  37335  inidl  37362  xrninxpex  37728  oposlem  38516  hlsuprexch  38716  ldilcnv  39450  ltrnu  39456  tgrpgrplem  40084  tgrpabl  40086  erngdvlem3  40325  erngdvlem3-rN  40333  dvalveclem  40360  dvhfvadd  40426  dvhgrp  40442  dvhlveclem  40443  djhval2  40734  f1o2d2  41522  fmpocos  41523  resubadd  41715  diophren  42014  monotoddzzfi  42144  ltrmynn0  42150  ltrmxnn0  42151  lermxnn0  42152  rmyeq  42156  lermy  42157  jm2.21  42196  radcnvrat  43536  dvconstbi  43556  expgrowth  43557  bi3impb  43707  eel132  43926  xlimmnfvlem2  45008  xlimpnfvlem2  45012  fnotaovb  46365  onetansqsecsq  47968