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  3281  vtocl3gf  3533  vtocl3g  3535  rspc2ev  3589  reuss  4273  cotsexgw  5463  frc  5614  trssord  6378  funtp  6595  resdif  6844  f1cdmsn  7288  f1ofvswap  7312  fnotovb  7470  fovcdm  7589  fnovrn  7594  fmpoco  8104  mpof1o2d  8135  smoord  8366  odi  8580  oeoa  8599  oeoe  8601  nndi  8625  ecopovtrn  8834  ecovass  8838  ecovdi  8839  unfi  9179  entrfil  9193  domtrfil  9200  f1imaenfi  9203  suppr  9457  infpr  9490  harval2  10071  fin23lem31  10414  tskuni  10861  addasspi  10973  mulasspi  10975  distrpi  10976  mulcanenq  11038  genpass  11087  distrlem1pr  11103  prlem934  11111  ltapr  11123  le2tri3i  11433  subadd  11553  addsub  11561  subdi  11742  submul2  11749  ltaddsub  11783  leaddsub  11785  divval  11969  diveq0  11977  div12  11989  diveq1  11996  divneg  12001  divdiv2  12022  ltmulgt11  12169  gt0div  12176  ge0div  12177  uzind3  12786  fnn0ind  12791  qdivcl  13091  irrmul  13095  xrlttr  13262  fzen  13667  modcyc  14039  modcyc2  14040  rpexpmord  14304  faclbnd4lem4  14433  ccatval21sw  14724  lswccatn0lsw  14731  ccatpfx  14843  ccatopth  14858  cshweqdifid  14964  lenegsq  15481  moddvds  16426  dvdscmulr  16447  dvdsmulcr  16448  dvds2add  16453  dvds2sub  16454  dvdsleabs  16474  divalg  16566  divalgb  16567  ndvdsadd  16573  gcdcllem3  16664  dvdslegcd  16667  modgcd  16698  absmulgcd  16715  odzval  16962  pcmul  17022  ressid2  17405  ressval2  17406  catcisolem  18278  prf1st  18371  prf2nd  18372  1st2ndprf  18373  curfuncf  18405  curf2ndf  18414  pltval  18497  pospo  18510  lubel  18681  isdlat  18689  submgmcl  18889  prdssgrpd  18915  issubmnd  18946  prdsmndd  18957  submcl  19000  grpinvid1  19195  grpinvid2  19196  mulgp1  19310  ghmlin  19428  ghmsub  19431  odlem2  19746  gexlem2  19789  lsmvalx  19846  efgtval  19930  cmncom  20005  lssvnegcl  21224  islss3  21227  prdslmodd  21237  zntoslem  21855  evlslem2  22381  evlseu  22385  maducoeval2  22948  madutpos  22950  madugsum  22951  madurid  22952  m2cpminvid  23064  pm2mpghm  23127  unopn  23214  ntrss  23366  innei  23436  t1sep2  23680  metustsym  24867  cncfi  25208  rrxds  25707  quotval  26606  abelthlem2  26752  mudivsum  27850  padicabv  27950  nosupfv  28056  nosupres  28057  noinffv  28071  sltssepc  28150  divsval  28568  axsegconlem1  29488  loop1cycl  30737  nsnlplig  31076  nsnlpligALT  31077  grpoinvid1  31123  grpoinvid2  31124  grpodivval  31130  ablo4  31145  ablonncan  31151  nvnpcan  31251  nvmeq0  31253  nvabs  31267  imsdval  31281  ipval  31298  nmorepnf  31363  blo3i  31397  blometi  31398  ipasslem5  31430  hvmulcan  31667  his5  31681  his7  31685  his2sub2  31688  hhssabloilem  31856  hhssnv  31859  fh1  32213  fh2  32214  cm2j  32215  homcl  32341  homco1  32396  homulass  32397  hoadddi  32398  hosubsub2  32407  braadd  32540  bramul  32541  lnopmul  32562  lnopli  32563  lnopaddmuli  32568  lnopsubmuli  32570  lnfnli  32635  lnfnaddmuli  32640  kbass2  32712  mdexchi  32930  xdivval  33478  resvid2  33884  resvval2  33885  fedgmullem2  34255  unitdivcld  34526  bnj229  35507  bnj546  35519  bnj570  35528  rankfilimb  35717  cusgredgex2  35886  cvmlift2lem7  36053  finminlem  37086  ivthALT  37103  topdifinffinlem  38250  lindsadd  38516  exidcl  38790  grposnOLD  38796  rngoneglmul  38857  rngonegrmul  38858  divrngcl  38871  crngocom  38915  crngm4  38917  inidl  38944  xrninxpex  39329  oposlem  40219  hlsuprexch  40418  ldilcnv  41152  ltrnu  41158  tgrpgrplem  41786  tgrpabl  41788  erngdvlem3  42027  erngdvlem3-rN  42035  dvalveclem  42062  dvhfvadd  42128  dvhgrp  42144  dvhlveclem  42145  djhval2  42436  fmpocos  43267  resubadd  43410  diophren  43799  monotoddzzfi  43928  ltrmynn0  43934  ltrmxnn0  43935  lermxnn0  43936  rmyeq  43940  lermy  43941  jm2.21  43980  radcnvrat  45283  dvconstbi  45303  expgrowth  45304  bi3impb  45452  xlimmnfvlem2  46812  xlimpnfvlem2  46816  fnotaovb  48237  tposcurf1  50376  precofvalALT  50445  onetansqsecsq  50823