Theorem ad3antlr 744

Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad3antlr	⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem ad3antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 487	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad2antrr 739	1 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

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

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

This theorem is used by:  simpllr  788  disjxiun  5099  fimaproj  8130  tfrlem1  8361  oaass  8547  acndom2  10105  infxp  10264  isf32lem2  10404  ttukeylem3  10561  gchina  10756  r1limwun  10793  difreicc  13585  ssfzo12bi  13865  flflp1  13916  hasheqf1oi  14463  ccatcl  14687  cshwidxmodr  14923  wwlktovf1  15078  sgnmul  15228  o1of2  15748  rlimsqzlem  15784  lcmgcdlem  16744  isprm5  16846  ramval  17148  mreexexlem4d  17783  acsfn  17795  chnso  18760  gsumpropd2lem  18830  issubmgm2  18854  gasubg  19478  omndmul2  20309  isdrng4  20954  unichnlidl  21478  qsidomlem1  21598  psgndiflemB  21868  psgndiflemA  21869  psrass1  22233  mhpmulcl  22432  mdetf  22872  matunitlindflem2  22957  cpmatacl  22996  cpmatinvcl  22997  mat2pmatf1  23009  mp2pm2mplem4  23089  chfacffsupp  23136  restcld  23452  cnpnei  23544  iscncl  23549  cncls  23554  cnntr  23555  1stcfb  23725  2ndcdisj  23737  txlly  23917  fbflim  24257  fclsbas  24302  nmoi  25009  mpomulcn  25150  fgcfil  25554  equivcau  25583  cmetcusp  25637  itg2cnlem1  26044  iblss  26087  lgsqr  27642  lgsqrmodndvds  27644  noetainflem4  28031  lesrec  28119  remulscllem2  28821  axcontlem2  29477  nbuhgr  29858  nbusgrvtxm1  29894  2pthon3v  30466  clwwisshclwwslem  30539  wwlksext2clwwlk  30582  2pthfrgr  30819  vdgn1frgrv2  30831  frgrwopreg  30858  numclwlk2lem2f1o  30914  blocnilem  31340  mdslmd3i  32868  foresf1o  33034  2ndresdju  33177  fgreu  33199  fdifsuppconst  33216  resf1o  33256  psgnfzto1st  33600  elrgspnsubrunlem1  33742  nsgqusf1olem3  33900  elrspunidl  33912  elrspunsn  33913  dflringlem3  33962  dflring4  33964  1arithidom  34003  dfufd2lem  34015  mplvrpmga  34111  lbsdiflsp0  34192  evls1fldgencl  34236  cos9thpiminplylem2  34349  ist0cld  34399  locfinreflem  34406  cmpcref  34416  zarclsun  34436  pstmxmet  34463  lmdvg  34519  carsgclctunlem3  34887  oddpwdc  34921  signstres  35139  tgoldbachgtd  35226  cvmlift2lem12  36000  satfdmlem  36054  satffunlem2lem1  36090  mrsubff  36198  elicc3  37027  nn0prpwlem  37032  neibastop2  37071  neibastop3  37072  mh-inf3f1  37251  bj-prmoore  37956  ltflcei  38451  poimirlem4  38462  poimirlem13  38471  poimirlem14  38472  poimirlem26  38484  poimirlem27  38485  poimirlem28  38486  poimirlem29  38487  poimirlem31  38489  heicant  38493  mblfinlem2  38496  mblfinlem3  38497  mblfinlem4  38498  ismblfin  38499  itg2addnclem  38509  itg2addnclem2  38510  itg2addnclem3  38511  itg2addnc  38512  itg2gt0cn  38513  ftc1cnnc  38530  ftc1anclem5  38535  ftc1anclem6  38536  ftc1anclem7  38537  ftc1anclem8  38538  ftc1anc  38539  nnubfi  38604  nninfnub  38605  linepsubN  40729  lhpmatb  41008  cdlemf2  41539  diaglbN  42032  diaintclN  42035  dibglbN  42143  dibintclN  42144  dihlsscpre  42211  dihglblem5aN  42269  dihglblem2aN  42270  dih1dimatlem  42306  sticksstones12a  43127  fsuppind  43540  diophren  43758  irrapxlem2  43768  irrapxlem4  43770  wepwsolem  43987  omlimcl2  44187  tfsconcatfv  44286  ofoafg  44299  prmunb2  45239  cvgdvgrat  45241  fiiuncl  46003  infleinflem2  46304  supxrunb3  46332  supminfxr  46396  limsuppnflem  46642  limsupmnflem  46652  limsupre3lem  46664  dfxlim2v  46779  icccncfext  46819  ioodvbdlimc1lem1  46863  iblcncfioo  46910  wallispilem3  46999  fourierdlem12  47051  fourierdlem34  47073  fourierdlem50  47088  fourierdlem51  47089  fourierdlem65  47103  fourierdlem77  47115  meaiuninc3v  47416  hspdifhsp  47548  smflimlem4  47706  iccpartigtl  48427  iccpartgt  48431  fargshiftfva  48447  sfprmdvdsmersenne  48610  opoeALTV  48703  opeoALTV  48704  nnsum4primeseven  48820  nnsum4primesevenALTV  48821  uhgrimedgi  48910  isuspgrimlem  48915  gricushgr  48937  isubgr3stgrlem7  48992  uspgrlimlem4  49011  gpgedgvtx1  49082  pgn4cyclex  49146  uzlidlring  49254  2zrngmmgm  49271  cznrng  49280  ply1mulgsumlem2  49421  snlindsntor  49505  elbigo2  49586  nn0sumshdiglemA  49653  precofvalALT  50398