Theorem 3impb 1132

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adant3  1150  syl3an132  1184  3impdi  1369  rsp2e  3285  vtocl3gf  3539  vtocl3g  3541  rspc2ev  3596  reuss  4280  frc  5626  trssord  6381  funtp  6597  resdif  6846  f1cdmsn  7286  f1ofvswap  7310  fnotovb  7468  fovcdm  7586  fnovrn  7591  fmpoco  8092  mpof1o2d  8123  smoord  8354  odi  8566  oeoa  8585  oeoe  8587  nndi  8611  ecopovtrn  8820  ecovass  8824  ecovdi  8825  unfi  9158  entrfil  9172  domtrfil  9179  f1imaenfi  9182  suppr  9435  infpr  9468  harval2  9995  fin23lem31  10338  tskuni  10779  addasspi  10891  mulasspi  10893  distrpi  10894  mulcanenq  10956  genpass  11005  distrlem1pr  11021  prlem934  11029  ltapr  11041  le2tri3i  11351  subadd  11471  addsub  11479  subdi  11658  submul2  11665  ltaddsub  11699  leaddsub  11701  divval  11885  diveq0  11893  div12  11905  diveq1  11912  divneg  11917  divdiv2  11938  ltmulgt11  12085  gt0div  12092  ge0div  12093  uzind3  12701  fnn0ind  12706  qdivcl  13005  irrmul  13009  xrlttr  13176  fzen  13580  modcyc  13952  modcyc2  13953  rpexpmord  14217  faclbnd4lem4  14345  ccatval21sw  14636  lswccatn0lsw  14643  ccatpfx  14755  ccatopth  14770  cshweqdifid  14876  lenegsq  15391  moddvds  16338  dvdscmulr  16359  dvdsmulcr  16360  dvds2add  16365  dvds2sub  16366  dvdsleabs  16386  divalg  16478  divalgb  16479  ndvdsadd  16485  gcdcllem3  16576  dvdslegcd  16579  modgcd  16607  absmulgcd  16624  odzval  16868  pcmul  16928  ressid2  17311  ressval2  17312  catcisolem  18184  prf1st  18277  prf2nd  18278  1st2ndprf  18279  curfuncf  18311  curf2ndf  18320  pltval  18403  pospo  18416  lubel  18587  isdlat  18595  submgmcl  18786  prdssgrpd  18812  issubmnd  18840  prdsmndd  18851  submcl  18893  grpinvid1  19081  grpinvid2  19082  mulgp1  19196  ghmlin  19314  ghmsub  19317  odlem2  19632  gexlem2  19675  lsmvalx  19732  efgtval  19816  cmncom  19891  lssvnegcl  21106  islss3  21109  prdslmodd  21119  zntoslem  21735  evlslem2  22259  evlseu  22263  maducoeval2  22826  madutpos  22828  madugsum  22829  madurid  22830  m2cpminvid  22939  pm2mpghm  23002  unopn  23089  ntrss  23241  innei  23311  t1sep2  23555  metustsym  24741  cncfi  25082  rrxds  25581  quotval  26482  abelthlem2  26624  mudivsum  27723  padicabv  27823  nosupfv  27899  nosupres  27900  noinffv  27914  sltssepc  27993  divsval  28411  axsegconlem1  29296  nsnlplig  30862  nsnlpligALT  30863  grpoinvid1  30909  grpoinvid2  30910  grpodivval  30916  ablo4  30931  ablonncan  30937  nvnpcan  31037  nvmeq0  31039  nvabs  31053  imsdval  31067  ipval  31084  nmorepnf  31149  blo3i  31183  blometi  31184  ipasslem5  31216  hvmulcan  31453  his5  31467  his7  31471  his2sub2  31474  hhssabloilem  31642  hhssnv  31645  fh1  31999  fh2  32000  cm2j  32001  homcl  32127  homco1  32182  homulass  32183  hoadddi  32184  hosubsub2  32193  braadd  32326  bramul  32327  lnopmul  32348  lnopli  32349  lnopaddmuli  32354  lnopsubmuli  32356  lnfnli  32421  lnfnaddmuli  32426  kbass2  32498  mdexchi  32716  xdivval  33267  resvid2  33673  resvval2  33674  fedgmullem2  34043  unitdivcld  34314  bnj229  35296  bnj546  35308  bnj570  35317  rankfilimb  35513  cusgredgex2  35628  loop1cycl  35642  cvmlift2lem7  35814  finminlem  36862  ivthALT  36879  topdifinffinlem  38026  lindsadd  38297  exidcl  38560  grposnOLD  38566  rngoneglmul  38627  rngonegrmul  38628  divrngcl  38641  crngocom  38685  crngm4  38687  inidl  38714  xrninxpex  39099  oposlem  39989  hlsuprexch  40188  ldilcnv  40922  ltrnu  40928  tgrpgrplem  41556  tgrpabl  41558  erngdvlem3  41797  erngdvlem3-rN  41805  dvalveclem  41832  dvhfvadd  41898  dvhgrp  41914  dvhlveclem  41915  djhval2  42206  fmpocos  43037  resubadd  43173  diophren  43573  monotoddzzfi  43702  ltrmynn0  43708  ltrmxnn0  43709  lermxnn0  43710  rmyeq  43714  lermy  43715  jm2.21  43754  radcnvrat  45057  dvconstbi  45077  expgrowth  45078  bi3impb  45226  xlimmnfvlem2  46580  xlimpnfvlem2  46584  fnotaovb  47968  tposcurf1  50110  precofvalALT  50179  onetansqsecsq  50572