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  776  disjxiun  5144  fimaproj  8158  tfrlem1  8414  oaass  8597  undomOLD  9098  acndom2  10091  infxp  10251  isf32lem2  10391  ttukeylem3  10548  gchina  10736  r1limwun  10773  difreicc  13520  ssfzo12bi  13796  flflp1  13843  hasheqf1oi  14386  ccatcl  14608  cshwidxmodr  14838  wwlktovf1  14992  o1of2  15645  rlimsqzlem  15681  lcmgcdlem  16639  isprm5  16740  ramval  17041  mreexexlem4d  17691  acsfn  17703  gsumpropd2lem  18704  issubmgm2  18728  gasubg  19332  psgndiflemB  21635  psgndiflemA  21636  psrass1  22001  mhpmulcl  22170  mdetf  22616  cpmatacl  22737  cpmatinvcl  22738  mat2pmatf1  22750  mp2pm2mplem4  22830  chfacffsupp  22877  restcld  23195  cnpnei  23287  iscncl  23292  cncls  23297  cnntr  23298  1stcfb  23468  2ndcdisj  23479  txlly  23659  fbflim  23999  fclsbas  24044  nmoi  24764  mpomulcn  24904  fgcfil  25318  equivcau  25347  cmetcusp  25401  itg2cnlem1  25810  iblss  25854  lgsqr  27409  lgsqrmodndvds  27411  noetainflem4  27799  slerec  27878  remulscllem2  28447  axcontlem2  28994  nbuhgr  29374  nbusgrvtxm1  29410  2pthon3v  29972  clwwisshclwwslem  30042  wwlksext2clwwlk  30085  2pthfrgr  30312  vdgn1frgrv2  30324  frgrwopreg  30351  numclwlk2lem2f1o  30407  blocnilem  30832  mdslmd3i  32360  foresf1o  32531  2ndresdju  32665  fgreu  32688  fdifsuppconst  32703  resf1o  32747  chnso  32987  omndmul2  33071  psgnfzto1st  33107  isdrng4  33278  nsgqusf1olem3  33422  elrspunidl  33435  elrspunsn  33436  qsidomlem1  33459  1arithidom  33544  dfufd2lem  33556  lbsdiflsp0  33653  evls1fldgencl  33694  ist0cld  33793  locfinreflem  33800  cmpcref  33810  zarclsun  33830  pstmxmet  33857  lmdvg  33913  carsgclctunlem3  34301  oddpwdc  34335  sgnmul  34523  signstres  34568  tgoldbachgtd  34655  cvmlift2lem12  35298  satfdmlem  35352  satffunlem2lem1  35388  mrsubff  35496  elicc3  36299  nn0prpwlem  36304  neibastop2  36343  neibastop3  36344  bj-prmoore  37097  ltflcei  37594  matunitlindflem2  37603  poimirlem4  37610  poimirlem13  37619  poimirlem14  37620  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  poimirlem29  37635  poimirlem31  37637  heicant  37641  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  itg2addnclem  37657  itg2addnclem2  37658  itg2addnclem3  37659  itg2addnc  37660  itg2gt0cn  37661  ftc1cnnc  37678  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  nnubfi  37736  nninfnub  37737  linepsubN  39734  lhpmatb  40013  cdlemf2  40544  diaglbN  41037  diaintclN  41040  dibglbN  41148  dibintclN  41149  dihlsscpre  41216  dihglblem5aN  41274  dihglblem2aN  41275  dih1dimatlem  41311  sticksstones12a  42138  fsuppind  42576  diophren  42800  irrapxlem2  42810  irrapxlem4  42812  wepwsolem  43030  omlimcl2  43230  tfsconcatfv  43330  ofoafg  43343  prmunb2  44306  cvgdvgrat  44308  fiiuncl  45004  infleinflem2  45320  supxrunb3  45348  supminfxr  45413  limsuppnflem  45665  limsupmnflem  45675  limsupre3lem  45687  dfxlim2v  45802  icccncfext  45842  ioodvbdlimc1lem1  45886  iblcncfioo  45933  wallispilem3  46022  fourierdlem12  46074  fourierdlem34  46096  fourierdlem50  46111  fourierdlem51  46112  fourierdlem65  46126  fourierdlem77  46138  meaiuninc3v  46439  hoicvr  46503  hspdifhsp  46571  smflimlem4  46729  iccpartigtl  47347  iccpartgt  47351  fargshiftfva  47367  sfprmdvdsmersenne  47527  opoeALTV  47607  opeoALTV  47608  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  isuspgrimlem  47811  gricushgr  47823  isubgr3stgrlem7  47874  uspgrlimlem4  47893  gpgedgvtx1  47954  uzlidlring  48078  2zrngmmgm  48095  cznrng  48104  ply1mulgsumlem2  48232  snlindsntor  48316  elbigo2  48401  nn0sumshdiglemA  48468