Theorem 3impb 1115

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 1111	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3adant3  1132  3impdi  1350  rsp2e  3284  vtocl3gf  3585  vtocl3g  3587  rspc2ev  3648  reuss  4346  frc  5663  trssord  6412  funtp  6635  resdif  6883  f1cdmsn  7318  f1ofvswap  7342  fnotovb  7500  fovcdm  7620  fnovrn  7625  fmpoco  8136  smoord  8421  odi  8635  oeoa  8653  oeoe  8655  nndi  8679  ecopovtrn  8878  ecovass  8882  ecovdi  8883  unfi  9238  entrfil  9251  domtrfil  9258  f1imaenfi  9261  suppr  9540  infpr  9572  harval2  10066  fin23lem31  10412  tskuni  10852  addasspi  10964  mulasspi  10966  distrpi  10967  mulcanenq  11029  genpass  11078  distrlem1pr  11094  prlem934  11102  ltapr  11114  le2tri3i  11420  subadd  11539  addsub  11547  subdi  11723  submul2  11730  ltaddsub  11764  leaddsub  11766  divval  11951  diveq0  11959  div12  11971  diveq1  11979  divneg  11986  divdiv2  12006  ltmulgt11  12154  gt0div  12161  ge0div  12162  uzind3  12737  fnn0ind  12742  qdivcl  13035  irrmul  13039  xrlttr  13202  fzen  13601  modcyc  13957  modcyc2  13958  rpexpmord  14218  faclbnd4lem4  14345  ccatval21sw  14633  lswccatn0lsw  14639  ccatpfx  14749  ccatopth  14764  cshweqdifid  14868  lenegsq  15369  moddvds  16313  dvdscmulr  16333  dvdsmulcr  16334  dvds2add  16338  dvds2sub  16339  dvdsleabs  16359  divalg  16451  divalgb  16452  ndvdsadd  16458  gcdcllem3  16547  dvdslegcd  16550  modgcd  16579  absmulgcd  16596  odzval  16838  pcmul  16898  ressid2  17291  ressval2  17292  catcisolem  18177  prf1st  18273  prf2nd  18274  1st2ndprf  18275  curfuncf  18308  curf2ndf  18317  pltval  18402  pospo  18415  lubel  18584  isdlat  18592  submgmcl  18745  prdssgrpd  18771  issubmnd  18799  prdsmndd  18805  submcl  18847  grpinvid1  19031  grpinvid2  19032  mulgp1  19147  ghmlin  19261  ghmsub  19264  odlem2  19581  gexlem2  19624  lsmvalx  19681  efgtval  19765  cmncom  19840  lssvnegcl  20977  islss3  20980  prdslmodd  20990  zntoslem  21598  evlslem2  22126  evlseu  22130  maducoeval2  22667  madutpos  22669  madugsum  22670  madurid  22671  m2cpminvid  22780  pm2mpghm  22843  unopn  22930  ntrss  23084  innei  23154  t1sep2  23398  metustsym  24589  cncfi  24939  rrxds  25446  quotval  26352  abelthlem2  26494  mudivsum  27592  padicabv  27692  nosupfv  27769  nosupres  27770  noinffv  27784  ssltsepc  27856  divsval  28233  axsegconlem1  28950  nsnlplig  30513  nsnlpligALT  30514  grpoinvid1  30560  grpoinvid2  30561  grpodivval  30567  ablo4  30582  ablonncan  30588  nvnpcan  30688  nvmeq0  30690  nvabs  30704  imsdval  30718  ipval  30735  nmorepnf  30800  blo3i  30834  blometi  30835  ipasslem5  30867  hvmulcan  31104  his5  31118  his7  31122  his2sub2  31125  hhssabloilem  31293  hhssnv  31296  fh1  31650  fh2  31651  cm2j  31652  homcl  31778  homco1  31833  homulass  31834  hoadddi  31835  hosubsub2  31844  braadd  31977  bramul  31978  lnopmul  31999  lnopli  32000  lnopaddmuli  32005  lnopsubmuli  32007  lnfnli  32072  lnfnaddmuli  32077  kbass2  32149  mdexchi  32367  xdivval  32883  resvid2  33319  resvval2  33320  fedgmullem2  33643  unitdivcld  33847  bnj229  34860  bnj546  34872  bnj570  34881  cusgredgex2  35090  loop1cycl  35105  cvmlift2lem7  35277  finminlem  36284  ivthALT  36301  topdifinffinlem  37313  lindsadd  37573  exidcl  37836  grposnOLD  37842  rngoneglmul  37903  rngonegrmul  37904  divrngcl  37917  crngocom  37961  crngm4  37963  inidl  37990  xrninxpex  38350  oposlem  39138  hlsuprexch  39338  ldilcnv  40072  ltrnu  40078  tgrpgrplem  40706  tgrpabl  40708  erngdvlem3  40947  erngdvlem3-rN  40955  dvalveclem  40982  dvhfvadd  41048  dvhgrp  41064  dvhlveclem  41065  djhval2  41356  f1o2d2  42228  fmpocos  42229  resubadd  42355  diophren  42769  monotoddzzfi  42899  ltrmynn0  42905  ltrmxnn0  42906  lermxnn0  42907  rmyeq  42911  lermy  42912  jm2.21  42951  radcnvrat  44283  dvconstbi  44303  expgrowth  44304  bi3impb  44454  eel132  44673  xlimmnfvlem2  45754  xlimpnfvlem2  45758  fnotaovb  47113  onetansqsecsq  48853