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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  3adant3  1150  syl3an132  1184  3impdi  1369  rsp2e  3283  vtocl3gf  3538  vtocl3g  3540  rspc2ev  3595  reuss  4281  frc  5626  trssord  6379  funtp  6595  resdif  6844  f1cdmsn  7282  f1ofvswap  7306  fnotovb  7464  fovcdm  7582  fnovrn  7587  fmpoco  8091  mpof1o2d  8122  smoord  8353  odi  8565  oeoa  8584  oeoe  8586  nndi  8610  ecopovtrn  8819  ecovass  8823  ecovdi  8824  unfi  9156  entrfil  9170  domtrfil  9177  f1imaenfi  9180  suppr  9433  infpr  9466  harval2  9984  fin23lem31  10328  tskuni  10769  addasspi  10881  mulasspi  10883  distrpi  10884  mulcanenq  10946  genpass  10995  distrlem1pr  11011  prlem934  11019  ltapr  11031  le2tri3i  11341  subadd  11461  addsub  11469  subdi  11648  submul2  11655  ltaddsub  11689  leaddsub  11691  divval  11875  diveq0  11883  div12  11895  diveq1  11902  divneg  11907  divdiv2  11928  ltmulgt11  12075  gt0div  12082  ge0div  12083  uzind3  12691  fnn0ind  12696  qdivcl  12995  irrmul  12999  xrlttr  13166  fzen  13570  modcyc  13941  modcyc2  13942  rpexpmord  14206  faclbnd4lem4  14334  ccatval21sw  14625  lswccatn0lsw  14631  ccatpfx  14740  ccatopth  14755  cshweqdifid  14859  lenegsq  15374  moddvds  16322  dvdscmulr  16343  dvdsmulcr  16344  dvds2add  16349  dvds2sub  16350  dvdsleabs  16370  divalg  16462  divalgb  16463  ndvdsadd  16469  gcdcllem3  16560  dvdslegcd  16563  modgcd  16591  absmulgcd  16608  odzval  16852  pcmul  16912  ressid2  17295  ressval2  17296  catcisolem  18168  prf1st  18261  prf2nd  18262  1st2ndprf  18263  curfuncf  18295  curf2ndf  18304  pltval  18387  pospo  18400  lubel  18571  isdlat  18579  submgmcl  18766  prdssgrpd  18792  issubmnd  18820  prdsmndd  18829  submcl  18871  grpinvid1  19059  grpinvid2  19060  mulgp1  19174  ghmlin  19292  ghmsub  19295  odlem2  19610  gexlem2  19653  lsmvalx  19710  efgtval  19794  cmncom  19869  lssvnegcl  21058  islss3  21061  prdslmodd  21071  zntoslem  21687  evlslem2  22211  evlseu  22215  maducoeval2  22778  madutpos  22780  madugsum  22781  madurid  22782  m2cpminvid  22891  pm2mpghm  22954  unopn  23041  ntrss  23193  innei  23263  t1sep2  23507  metustsym  24693  cncfi  25034  rrxds  25533  quotval  26434  abelthlem2  26576  mudivsum  27675  padicabv  27775  nosupfv  27851  nosupres  27852  noinffv  27866  sltssepc  27945  divsval  28363  axsegconlem1  29248  nsnlplig  30814  nsnlpligALT  30815  grpoinvid1  30861  grpoinvid2  30862  grpodivval  30868  ablo4  30883  ablonncan  30889  nvnpcan  30989  nvmeq0  30991  nvabs  31005  imsdval  31019  ipval  31036  nmorepnf  31101  blo3i  31135  blometi  31136  ipasslem5  31168  hvmulcan  31405  his5  31419  his7  31423  his2sub2  31426  hhssabloilem  31594  hhssnv  31597  fh1  31951  fh2  31952  cm2j  31953  homcl  32079  homco1  32134  homulass  32135  hoadddi  32136  hosubsub2  32145  braadd  32278  bramul  32279  lnopmul  32300  lnopli  32301  lnopaddmuli  32306  lnopsubmuli  32308  lnfnli  32373  lnfnaddmuli  32378  kbass2  32450  mdexchi  32668  xdivval  33219  resvid2  33631  resvval2  33632  fedgmullem2  34001  unitdivcld  34272  bnj229  35253  bnj546  35265  bnj570  35274  rankfilimb  35477  cusgredgex2  35596  loop1cycl  35610  cvmlift2lem7  35782  finminlem  36810  ivthALT  36827  topdifinffinlem  37974  lindsadd  38245  exidcl  38508  grposnOLD  38514  rngoneglmul  38575  rngonegrmul  38576  divrngcl  38589  crngocom  38633  crngm4  38635  inidl  38662  xrninxpex  39047  oposlem  39937  hlsuprexch  40136  ldilcnv  40870  ltrnu  40876  tgrpgrplem  41504  tgrpabl  41506  erngdvlem3  41745  erngdvlem3-rN  41753  dvalveclem  41780  dvhfvadd  41846  dvhgrp  41862  dvhlveclem  41863  djhval2  42154  fmpocos  42985  resubadd  43121  diophren  43523  monotoddzzfi  43652  ltrmynn0  43658  ltrmxnn0  43659  lermxnn0  43660  rmyeq  43664  lermy  43665  jm2.21  43704  radcnvrat  45007  dvconstbi  45027  expgrowth  45028  bi3impb  45176  xlimmnfvlem2  46530  xlimpnfvlem2  46534  fnotaovb  47918  tposcurf1  50060  precofvalALT  50129  onetansqsecsq  50522