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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  simpllr  774  disjxiun  5145  fimaproj  8138  tfrlem1  8395  oaass  8580  undomOLD  9083  acndom2  10077  infxp  10238  isf32lem2  10377  ttukeylem3  10534  gchina  10722  r1limwun  10759  difreicc  13493  ssfzo12bi  13759  flflp1  13804  hasheqf1oi  14342  ccatcl  14556  cshwidxmodr  14786  wwlktovf1  14940  o1of2  15589  rlimsqzlem  15627  lcmgcdlem  16576  isprm5  16677  ramval  16976  mreexexlem4d  17626  acsfn  17638  gsumpropd2lem  18638  issubmgm2  18662  gasubg  19257  psgndiflemB  21536  psgndiflemA  21537  psrass1  21913  mdetf  22527  cpmatacl  22648  cpmatinvcl  22649  mat2pmatf1  22661  mp2pm2mplem4  22741  chfacffsupp  22788  restcld  23106  cnpnei  23198  iscncl  23203  cncls  23208  cnntr  23209  1stcfb  23379  2ndcdisj  23390  txlly  23570  fbflim  23910  fclsbas  23955  nmoi  24675  mpomulcn  24815  fgcfil  25229  equivcau  25258  cmetcusp  25312  itg2cnlem1  25721  iblss  25764  lgsqr  27314  lgsqrmodndvds  27316  noetainflem4  27703  slerec  27782  remulscllem2  28285  axcontlem2  28832  nbuhgr  29212  nbusgrvtxm1  29248  2pthon3v  29810  clwwisshclwwslem  29880  wwlksext2clwwlk  29923  2pthfrgr  30150  vdgn1frgrv2  30162  frgrwopreg  30189  numclwlk2lem2f1o  30245  blocnilem  30670  mdslmd3i  32198  foresf1o  32357  2ndresdju  32492  fgreu  32515  fdifsuppconst  32526  resf1o  32569  omndmul2  32849  psgnfzto1st  32883  isdrng4  33044  nsgqusf1olem3  33187  elrspunidl  33206  elrspunsn  33207  qsidomlem1  33230  lbsdiflsp0  33394  evls1fldgencl  33428  ist0cld  33504  locfinreflem  33511  cmpcref  33521  zarclsun  33541  pstmxmet  33568  lmdvg  33624  carsgclctunlem3  34010  oddpwdc  34044  sgnmul  34232  signstres  34277  tgoldbachgtd  34364  cvmlift2lem12  34994  satfdmlem  35048  satffunlem2lem1  35084  mrsubff  35192  elicc3  35871  nn0prpwlem  35876  neibastop2  35915  neibastop3  35916  bj-prmoore  36664  ltflcei  37151  matunitlindflem2  37160  poimirlem4  37167  poimirlem13  37176  poimirlem14  37177  poimirlem26  37189  poimirlem27  37190  poimirlem28  37191  poimirlem29  37192  poimirlem31  37194  heicant  37198  mblfinlem2  37201  mblfinlem3  37202  mblfinlem4  37203  ismblfin  37204  itg2addnclem  37214  itg2addnclem2  37215  itg2addnclem3  37216  itg2addnc  37217  itg2gt0cn  37218  ftc1cnnc  37235  ftc1anclem5  37240  ftc1anclem6  37241  ftc1anclem7  37242  ftc1anclem8  37243  ftc1anc  37244  nnubfi  37293  nninfnub  37294  linepsubN  39294  lhpmatb  39573  cdlemf2  40104  diaglbN  40597  diaintclN  40600  dibglbN  40708  dibintclN  40709  dihlsscpre  40776  dihglblem5aN  40834  dihglblem2aN  40835  dih1dimatlem  40871  sticksstones12a  41698  fsuppind  41888  diophren  42298  irrapxlem2  42308  irrapxlem4  42310  wepwsolem  42531  omlimcl2  42735  tfsconcatfv  42835  ofoafg  42848  prmunb2  43813  cvgdvgrat  43815  fiiuncl  44494  infleinflem2  44816  supxrunb3  44844  supminfxr  44909  limsuppnflem  45161  limsupmnflem  45171  limsupre3lem  45183  dfxlim2v  45298  icccncfext  45338  ioodvbdlimc1lem1  45382  iblcncfioo  45429  wallispilem3  45518  fourierdlem12  45570  fourierdlem34  45592  fourierdlem50  45607  fourierdlem51  45608  fourierdlem65  45622  fourierdlem77  45634  meaiuninc3v  45935  hoicvr  45999  hspdifhsp  46067  smflimlem4  46225  iccpartigtl  46826  iccpartgt  46830  fargshiftfva  46846  sfprmdvdsmersenne  47006  opoeALTV  47086  opeoALTV  47087  nnsum4primeseven  47203  nnsum4primesevenALTV  47204  isuspgrimlem  47284  gricushgr  47295  uzlidlring  47409  2zrngmmgm  47426  cznrng  47435  ply1mulgsumlem2  47567  snlindsntor  47651  elbigo2  47737  nn0sumshdiglemA  47804