Theorem 3impb 1112

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 424	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1108	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3adant3  1129  3impdi  1347  rsp2e  3264  vtocl3gf  3519  rspc2ev  3583  reuss  4236  frc  5485  trssord  6176  funtp  6381  resdif  6610  fnotovb  7185  fovrn  7298  fnovrn  7303  fmpoco  7773  smoord  7985  odi  8188  oeoa  8206  oeoe  8208  nndi  8232  ecopovtrn  8383  ecovass  8387  ecovdi  8388  suppr  8919  infpr  8951  harval2  9410  fin23lem31  9754  tskuni  10194  addasspi  10306  mulasspi  10308  distrpi  10309  mulcanenq  10371  genpass  10420  distrlem1pr  10436  prlem934  10444  ltapr  10456  le2tri3i  10759  subadd  10878  addsub  10886  subdi  11062  submul2  11069  ltaddsub  11103  leaddsub  11105  divval  11289  div12  11309  diveq1  11320  divneg  11321  divdiv2  11341  ltmulgt11  11489  gt0div  11495  ge0div  11496  uzind3  12064  fnn0ind  12069  qdivcl  12357  irrmul  12361  xrlttr  12521  fzen  12919  modcyc  13269  modcyc2  13270  rpexpmord  13528  faclbnd4lem4  13652  ccatval21sw  13930  lswccatn0lsw  13936  ccatpfx  14054  ccatopth  14069  cshweqdifid  14173  lenegsq  14672  moddvds  15610  dvdscmulr  15630  dvdsmulcr  15631  dvds2add  15635  dvds2sub  15636  dvdsleabs  15653  divalg  15744  divalgb  15745  ndvdsadd  15751  gcdcllem3  15840  dvdslegcd  15843  modgcd  15870  absmulgcd  15887  odzval  16118  pcmul  16178  ressid2  16544  ressval2  16545  catcisolem  17358  prf1st  17446  prf2nd  17447  1st2ndprf  17448  curfuncf  17480  curf2ndf  17489  pltval  17562  pospo  17575  lubel  17724  isdlat  17795  issubmnd  17930  prdsmndd  17936  submcl  17969  grpinvid1  18146  grpinvid2  18147  mulgp1  18252  ghmlin  18355  ghmsub  18358  odlem2  18659  gexlem2  18699  lsmvalx  18756  efgtval  18841  cmncom  18915  lssvnegcl  19721  islss3  19724  prdslmodd  19734  zntoslem  20248  evlslem2  20751  evlseu  20755  maducoeval2  21245  madutpos  21247  madugsum  21248  madurid  21249  m2cpminvid  21358  pm2mpghm  21421  unopn  21508  ntrss  21660  innei  21730  t1sep2  21974  metustsym  23162  cncfi  23499  rrxds  23997  quotval  24888  abelthlem2  25027  mudivsum  26114  padicabv  26214  axsegconlem1  26711  nsnlplig  28264  nsnlpligALT  28265  grpoinvid1  28311  grpoinvid2  28312  grpodivval  28318  ablo4  28333  ablonncan  28339  nvnpcan  28439  nvmeq0  28441  nvabs  28455  imsdval  28469  ipval  28486  nmorepnf  28551  blo3i  28585  blometi  28586  ipasslem5  28618  hvmulcan  28855  his5  28869  his7  28873  his2sub2  28876  hhssabloilem  29044  hhssnv  29047  fh1  29401  fh2  29402  cm2j  29403  homcl  29529  homco1  29584  homulass  29585  hoadddi  29586  hosubsub2  29595  braadd  29728  bramul  29729  lnopmul  29750  lnopli  29751  lnopaddmuli  29756  lnopsubmuli  29758  lnfnli  29823  lnfnaddmuli  29828  kbass2  29900  mdexchi  30118  xdivval  30621  resvid2  30952  resvval2  30953  fedgmullem2  31114  unitdivcld  31254  bnj229  32266  bnj546  32278  bnj570  32287  cusgredgex2  32482  loop1cycl  32497  cvmlift2lem7  32669  nosupfv  33319  nosupres  33320  finminlem  33779  ivthALT  33796  topdifinffinlem  34764  lindsadd  35050  exidcl  35314  grposnOLD  35320  rngoneglmul  35381  rngonegrmul  35382  divrngcl  35395  crngocom  35439  crngm4  35441  inidl  35468  xrninxpex  35802  oposlem  36478  hlsuprexch  36677  ldilcnv  37411  ltrnu  37417  tgrpgrplem  38045  tgrpabl  38047  erngdvlem3  38286  erngdvlem3-rN  38294  dvalveclem  38321  dvhfvadd  38387  dvhgrp  38403  dvhlveclem  38404  djhval2  38695  resubadd  39517  diophren  39754  monotoddzzfi  39883  ltrmynn0  39889  ltrmxnn0  39890  lermxnn0  39891  rmyeq  39895  lermy  39896  jm2.21  39935  radcnvrat  41018  dvconstbi  41038  expgrowth  41039  bi3impb  41189  eel132  41408  xlimmnfvlem2  42475  xlimpnfvlem2  42479  fnotaovb  43754  submgmcl  44414  onetansqsecsq  45287