Theorem ad3antlr 729

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  simpllr  774  disjxiun  5054  fimaproj  7821  tfrlem1  8004  oaass  8179  undom  8597  acndom2  9472  infxp  9629  isf32lem2  9768  ttukeylem3  9925  gchina  10113  r1limwun  10150  difreicc  12862  ssfzo12bi  13124  flflp1  13169  hasheqf1oi  13704  ccatcl  13918  cshwidxmodr  14158  wwlktovf1  14313  o1of2  14961  rlimsqzlem  14997  lcmgcdlem  15942  isprm5  16043  ramval  16336  mreexexlem4d  16910  acsfn  16922  gsumpropd2lem  17881  gasubg  18424  psgndiflemB  20736  psgndiflemA  20737  mdetf  21196  cpmatacl  21316  cpmatinvcl  21317  mat2pmatf1  21329  mp2pm2mplem4  21409  chfacffsupp  21456  restcld  21772  cnpnei  21864  iscncl  21869  cncls  21874  cnntr  21875  1stcfb  22045  2ndcdisj  22056  txlly  22236  fbflim  22576  fclsbas  22621  nmoi  23329  fgcfil  23866  equivcau  23895  cmetcusp  23949  itg2cnlem1  24354  iblss  24397  lgsqr  25919  lgsqrmodndvds  25921  axcontlem2  26743  nbuhgr  27117  nbusgrvtxm1  27153  2pthon3v  27714  clwwisshclwwslem  27784  wwlksext2clwwlk  27828  2pthfrgr  28055  vdgn1frgrv2  28067  frgrwopreg  28094  numclwlk2lem2f1o  28150  blocnilem  28573  mdslmd3i  30101  foresf1o  30257  fgreu  30409  resf1o  30458  omndmul2  30706  psgnfzto1st  30740  qsidomlem1  30958  lbsdiflsp0  31015  locfinreflem  31097  cmpcref  31107  pstmxmet  31130  lmdvg  31189  carsgclctunlem3  31571  oddpwdc  31605  sgnmul  31793  signstres  31838  tgoldbachgtd  31926  cvmlift2lem12  32554  satfdmlem  32608  satffunlem2lem1  32644  mrsubff  32752  slerec  33270  elicc3  33658  nn0prpwlem  33663  neibastop2  33702  neibastop3  33703  bj-prmoore  34399  ltflcei  34872  matunitlindflem2  34881  poimirlem4  34888  poimirlem13  34897  poimirlem14  34898  poimirlem26  34910  poimirlem27  34911  poimirlem28  34912  poimirlem29  34913  poimirlem31  34915  heicant  34919  mblfinlem2  34922  mblfinlem3  34923  mblfinlem4  34924  ismblfin  34925  itg2addnclem  34935  itg2addnclem2  34936  itg2addnclem3  34937  itg2addnc  34938  itg2gt0cn  34939  ftc1cnnc  34958  ftc1anclem5  34963  ftc1anclem6  34964  ftc1anclem7  34965  ftc1anclem8  34966  ftc1anc  34967  nnubfi  35017  nninfnub  35018  linepsubN  36880  lhpmatb  37159  cdlemf2  37690  diaglbN  38183  diaintclN  38186  dibglbN  38294  dibintclN  38295  dihlsscpre  38362  dihglblem5aN  38420  dihglblem2aN  38421  dih1dimatlem  38457  diophren  39401  irrapxlem2  39411  irrapxlem4  39413  wepwsolem  39633  prmunb2  40634  cvgdvgrat  40636  fiiuncl  41318  infleinflem2  41629  supxrunb3  41662  supminfxr  41730  limsuppnflem  41981  limsupmnflem  41991  limsupre3lem  42003  dfxlim2v  42118  icccncfext  42160  ioodvbdlimc1lem1  42206  iblcncfioo  42253  wallispilem3  42343  fourierdlem12  42395  fourierdlem34  42417  fourierdlem50  42432  fourierdlem51  42433  fourierdlem65  42447  fourierdlem77  42459  meaiuninc3v  42757  hoicvr  42821  hspdifhsp  42889  smflimlem4  43041  iccpartigtl  43574  iccpartgt  43578  fargshiftfva  43594  sfprmdvdsmersenne  43759  opoeALTV  43839  opeoALTV  43840  nnsum4primeseven  43956  nnsum4primesevenALTV  43957  isomushgr  43982  isomuspgr  43990  issubmgm2  44048  uzlidlring  44191  2zrngmmgm  44208  cznrng  44217  ply1mulgsumlem2  44432  snlindsntor  44517  elbigo2  44603  nn0sumshdiglemA  44670