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  5116  fimaproj  8132  tfrlem1  8388  oaass  8571  undomOLD  9072  acndom2  10066  infxp  10226  isf32lem2  10366  ttukeylem3  10523  gchina  10711  r1limwun  10748  difreicc  13499  ssfzo12bi  13775  flflp1  13822  hasheqf1oi  14367  ccatcl  14590  cshwidxmodr  14820  wwlktovf1  14974  o1of2  15627  rlimsqzlem  15663  lcmgcdlem  16623  isprm5  16724  ramval  17026  mreexexlem4d  17657  acsfn  17669  gsumpropd2lem  18655  issubmgm2  18679  gasubg  19283  psgndiflemB  21558  psgndiflemA  21559  psrass1  21922  mhpmulcl  22085  mdetf  22531  cpmatacl  22652  cpmatinvcl  22653  mat2pmatf1  22665  mp2pm2mplem4  22745  chfacffsupp  22792  restcld  23108  cnpnei  23200  iscncl  23205  cncls  23210  cnntr  23211  1stcfb  23381  2ndcdisj  23392  txlly  23572  fbflim  23912  fclsbas  23957  nmoi  24665  mpomulcn  24807  fgcfil  25221  equivcau  25250  cmetcusp  25304  itg2cnlem1  25712  iblss  25756  lgsqr  27312  lgsqrmodndvds  27314  noetainflem4  27702  slerec  27781  remulscllem2  28350  axcontlem2  28890  nbuhgr  29268  nbusgrvtxm1  29304  2pthon3v  29871  clwwisshclwwslem  29941  wwlksext2clwwlk  29984  2pthfrgr  30211  vdgn1frgrv2  30223  frgrwopreg  30250  numclwlk2lem2f1o  30306  blocnilem  30731  mdslmd3i  32259  foresf1o  32431  2ndresdju  32573  fgreu  32596  fdifsuppconst  32612  resf1o  32653  sgnmul  32760  chnso  32940  omndmul2  33026  psgnfzto1st  33062  elrgspnsubrunlem1  33188  isdrng4  33235  nsgqusf1olem3  33376  elrspunidl  33389  elrspunsn  33390  qsidomlem1  33413  1arithidom  33498  dfufd2lem  33510  lbsdiflsp0  33612  evls1fldgencl  33657  cos9thpiminplylem2  33763  ist0cld  33810  locfinreflem  33817  cmpcref  33827  zarclsun  33847  pstmxmet  33874  lmdvg  33930  carsgclctunlem3  34298  oddpwdc  34332  signstres  34553  tgoldbachgtd  34640  cvmlift2lem12  35282  satfdmlem  35336  satffunlem2lem1  35372  mrsubff  35480  elicc3  36281  nn0prpwlem  36286  neibastop2  36325  neibastop3  36326  bj-prmoore  37079  ltflcei  37578  matunitlindflem2  37587  poimirlem4  37594  poimirlem13  37603  poimirlem14  37604  poimirlem26  37616  poimirlem27  37617  poimirlem28  37618  poimirlem29  37619  poimirlem31  37621  heicant  37625  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  itg2addnclem  37641  itg2addnclem2  37642  itg2addnclem3  37643  itg2addnc  37644  itg2gt0cn  37645  ftc1cnnc  37662  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  nnubfi  37720  nninfnub  37721  linepsubN  39717  lhpmatb  39996  cdlemf2  40527  diaglbN  41020  diaintclN  41023  dibglbN  41131  dibintclN  41132  dihlsscpre  41199  dihglblem5aN  41257  dihglblem2aN  41258  dih1dimatlem  41294  sticksstones12a  42116  fsuppind  42560  diophren  42783  irrapxlem2  42793  irrapxlem4  42795  wepwsolem  43013  omlimcl2  43213  tfsconcatfv  43312  ofoafg  43325  prmunb2  44283  cvgdvgrat  44285  fiiuncl  45037  infleinflem2  45346  supxrunb3  45374  supminfxr  45439  limsuppnflem  45687  limsupmnflem  45697  limsupre3lem  45709  dfxlim2v  45824  icccncfext  45864  ioodvbdlimc1lem1  45908  iblcncfioo  45955  wallispilem3  46044  fourierdlem12  46096  fourierdlem34  46118  fourierdlem50  46133  fourierdlem51  46134  fourierdlem65  46148  fourierdlem77  46160  meaiuninc3v  46461  hoicvr  46525  hspdifhsp  46593  smflimlem4  46751  iccpartigtl  47385  iccpartgt  47389  fargshiftfva  47405  sfprmdvdsmersenne  47565  opoeALTV  47645  opeoALTV  47646  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  uhgrimedgi  47851  isuspgrimlem  47856  gricushgr  47878  isubgr3stgrlem7  47932  uspgrlimlem4  47951  gpgedgvtx1  48014  uzlidlring  48158  2zrngmmgm  48175  cznrng  48184  ply1mulgsumlem2  48311  snlindsntor  48395  elbigo2  48480  nn0sumshdiglemA  48547  precofvalALT  49227