Theorem ad3antlr 731

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 481	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad2antrr 726	1 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  simpllr  775  disjxiun  5092  fimaproj  8075  tfrlem1  8305  oaass  8486  acndom2  9967  infxp  10127  isf32lem2  10267  ttukeylem3  10424  gchina  10612  r1limwun  10649  difreicc  13405  ssfzo12bi  13682  flflp1  13729  hasheqf1oi  14276  ccatcl  14499  cshwidxmodr  14728  wwlktovf1  14882  o1of2  15538  rlimsqzlem  15574  lcmgcdlem  16535  isprm5  16636  ramval  16938  mreexexlem4d  17571  acsfn  17583  gsumpropd2lem  18571  issubmgm2  18595  gasubg  19199  omndmul2  20030  psgndiflemB  21525  psgndiflemA  21526  psrass1  21889  mhpmulcl  22052  mdetf  22498  cpmatacl  22619  cpmatinvcl  22620  mat2pmatf1  22632  mp2pm2mplem4  22712  chfacffsupp  22759  restcld  23075  cnpnei  23167  iscncl  23172  cncls  23177  cnntr  23178  1stcfb  23348  2ndcdisj  23359  txlly  23539  fbflim  23879  fclsbas  23924  nmoi  24632  mpomulcn  24774  fgcfil  25187  equivcau  25216  cmetcusp  25270  itg2cnlem1  25678  iblss  25722  lgsqr  27278  lgsqrmodndvds  27280  noetainflem4  27668  slerec  27748  remulscllem2  28388  axcontlem2  28928  nbuhgr  29306  nbusgrvtxm1  29342  2pthon3v  29906  clwwisshclwwslem  29976  wwlksext2clwwlk  30019  2pthfrgr  30246  vdgn1frgrv2  30258  frgrwopreg  30285  numclwlk2lem2f1o  30341  blocnilem  30766  mdslmd3i  32294  foresf1o  32466  2ndresdju  32606  fgreu  32629  fdifsuppconst  32645  resf1o  32686  sgnmul  32793  chnso  32969  psgnfzto1st  33060  elrgspnsubrunlem1  33197  isdrng4  33244  nsgqusf1olem3  33362  elrspunidl  33375  elrspunsn  33376  qsidomlem1  33399  1arithidom  33484  dfufd2lem  33496  lbsdiflsp0  33598  evls1fldgencl  33641  cos9thpiminplylem2  33749  ist0cld  33799  locfinreflem  33806  cmpcref  33816  zarclsun  33836  pstmxmet  33863  lmdvg  33919  carsgclctunlem3  34287  oddpwdc  34321  signstres  34542  tgoldbachgtd  34629  cvmlift2lem12  35286  satfdmlem  35340  satffunlem2lem1  35376  mrsubff  35484  elicc3  36290  nn0prpwlem  36295  neibastop2  36334  neibastop3  36335  bj-prmoore  37088  ltflcei  37587  matunitlindflem2  37596  poimirlem4  37603  poimirlem13  37612  poimirlem14  37613  poimirlem26  37625  poimirlem27  37626  poimirlem28  37627  poimirlem29  37628  poimirlem31  37630  heicant  37634  mblfinlem2  37637  mblfinlem3  37638  mblfinlem4  37639  ismblfin  37640  itg2addnclem  37650  itg2addnclem2  37651  itg2addnclem3  37652  itg2addnc  37653  itg2gt0cn  37654  ftc1cnnc  37671  ftc1anclem5  37676  ftc1anclem6  37677  ftc1anclem7  37678  ftc1anclem8  37679  ftc1anc  37680  nnubfi  37729  nninfnub  37730  linepsubN  39731  lhpmatb  40010  cdlemf2  40541  diaglbN  41034  diaintclN  41037  dibglbN  41145  dibintclN  41146  dihlsscpre  41213  dihglblem5aN  41271  dihglblem2aN  41272  dih1dimatlem  41308  sticksstones12a  42130  fsuppind  42563  diophren  42786  irrapxlem2  42796  irrapxlem4  42798  wepwsolem  43015  omlimcl2  43215  tfsconcatfv  43314  ofoafg  43327  prmunb2  44284  cvgdvgrat  44286  fiiuncl  45043  infleinflem2  45351  supxrunb3  45379  supminfxr  45444  limsuppnflem  45692  limsupmnflem  45702  limsupre3lem  45714  dfxlim2v  45829  icccncfext  45869  ioodvbdlimc1lem1  45913  iblcncfioo  45960  wallispilem3  46049  fourierdlem12  46101  fourierdlem34  46123  fourierdlem50  46138  fourierdlem51  46139  fourierdlem65  46153  fourierdlem77  46165  meaiuninc3v  46466  hoicvr  46530  hspdifhsp  46598  smflimlem4  46756  iccpartigtl  47408  iccpartgt  47412  fargshiftfva  47428  sfprmdvdsmersenne  47588  opoeALTV  47668  opeoALTV  47669  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  uhgrimedgi  47874  isuspgrimlem  47879  gricushgr  47901  isubgr3stgrlem7  47955  uspgrlimlem4  47974  gpgedgvtx1  48037  pgn4cyclex  48100  uzlidlring  48207  2zrngmmgm  48224  cznrng  48233  ply1mulgsumlem2  48360  snlindsntor  48444  elbigo2  48525  nn0sumshdiglemA  48592  precofvalALT  49341