Theorem ad3antlr 744

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simpllr  788  disjxiun  5104  fimaproj  8136  tfrlem1  8367  oaass  8551  acndom2  10060  infxp  10219  isf32lem2  10359  ttukeylem3  10516  gchina  10711  r1limwun  10748  difreicc  13539  ssfzo12bi  13819  flflp1  13870  hasheqf1oi  14417  ccatcl  14641  cshwidxmodr  14877  wwlktovf1  15032  sgnmul  15182  o1of2  15702  rlimsqzlem  15738  lcmgcdlem  16700  isprm5  16802  ramval  17104  mreexexlem4d  17739  acsfn  17751  chnso  18716  gsumpropd2lem  18785  issubmgm2  18809  gasubg  19433  omndmul2  20264  isdrng4  20906  unichnlidl  21429  qsidomlem1  21547  psgndiflemB  21817  psgndiflemA  21818  psrass1  22182  mhpmulcl  22381  mdetf  22821  matunitlindflem2  22906  cpmatacl  22945  cpmatinvcl  22946  mat2pmatf1  22958  mp2pm2mplem4  23038  chfacffsupp  23085  restcld  23401  cnpnei  23493  iscncl  23498  cncls  23503  cnntr  23504  1stcfb  23674  2ndcdisj  23686  txlly  23866  fbflim  24206  fclsbas  24251  nmoi  24958  mpomulcn  25099  fgcfil  25503  equivcau  25532  cmetcusp  25586  itg2cnlem1  25993  iblss  26037  lgsqr  27588  lgsqrmodndvds  27590  noetainflem4  27977  lesrec  28065  remulscllem2  28767  axcontlem2  29423  nbuhgr  29804  nbusgrvtxm1  29840  2pthon3v  30412  clwwisshclwwslem  30485  wwlksext2clwwlk  30528  2pthfrgr  30765  vdgn1frgrv2  30777  frgrwopreg  30804  numclwlk2lem2f1o  30860  blocnilem  31286  mdslmd3i  32814  foresf1o  32980  2ndresdju  33124  fgreu  33146  fdifsuppconst  33163  resf1o  33203  psgnfzto1st  33547  elrgspnsubrunlem1  33689  nsgqusf1olem3  33846  elrspunidl  33858  elrspunsn  33859  dflringlem3  33908  dflring4  33910  1arithidom  33949  dfufd2lem  33961  mplvrpmga  34057  lbsdiflsp0  34138  evls1fldgencl  34182  cos9thpiminplylem2  34295  ist0cld  34345  locfinreflem  34352  cmpcref  34362  zarclsun  34382  pstmxmet  34409  lmdvg  34465  carsgclctunlem3  34833  oddpwdc  34867  signstres  35085  tgoldbachgtd  35172  cvmlift2lem12  35895  satfdmlem  35949  satffunlem2lem1  35985  mrsubff  36093  elicc3  36938  nn0prpwlem  36943  neibastop2  36982  neibastop3  36983  bj-prmoore  37867  ltflcei  38364  poimirlem4  38375  poimirlem13  38384  poimirlem14  38385  poimirlem26  38397  poimirlem27  38398  poimirlem28  38399  poimirlem29  38400  poimirlem31  38402  heicant  38406  mblfinlem2  38409  mblfinlem3  38410  mblfinlem4  38411  ismblfin  38412  itg2addnclem  38422  itg2addnclem2  38423  itg2addnclem3  38424  itg2addnc  38425  itg2gt0cn  38426  ftc1cnnc  38443  ftc1anclem5  38448  ftc1anclem6  38449  ftc1anclem7  38450  ftc1anclem8  38451  ftc1anc  38452  nnubfi  38502  nninfnub  38503  linepsubN  40627  lhpmatb  40906  cdlemf2  41437  diaglbN  41930  diaintclN  41933  dibglbN  42041  dibintclN  42042  dihlsscpre  42109  dihglblem5aN  42167  dihglblem2aN  42168  dih1dimatlem  42204  sticksstones12a  43025  fsuppind  43438  diophren  43656  irrapxlem2  43666  irrapxlem4  43668  wepwsolem  43885  omlimcl2  44085  tfsconcatfv  44184  ofoafg  44197  prmunb2  45137  cvgdvgrat  45139  fiiuncl  45901  infleinflem2  46202  supxrunb3  46230  supminfxr  46294  limsuppnflem  46540  limsupmnflem  46550  limsupre3lem  46562  dfxlim2v  46677  icccncfext  46717  ioodvbdlimc1lem1  46761  iblcncfioo  46808  wallispilem3  46897  fourierdlem12  46949  fourierdlem34  46971  fourierdlem50  46986  fourierdlem51  46987  fourierdlem65  47001  fourierdlem77  47013  meaiuninc3v  47314  hspdifhsp  47446  smflimlem4  47604  iccpartigtl  48325  iccpartgt  48329  fargshiftfva  48345  sfprmdvdsmersenne  48508  opoeALTV  48601  opeoALTV  48602  nnsum4primeseven  48718  nnsum4primesevenALTV  48719  uhgrimedgi  48808  isuspgrimlem  48813  gricushgr  48835  isubgr3stgrlem7  48890  uspgrlimlem4  48909  gpgedgvtx1  48980  pgn4cyclex  49044  uzlidlring  49152  2zrngmmgm  49169  cznrng  49178  ply1mulgsumlem2  49319  snlindsntor  49403  elbigo2  49484  nn0sumshdiglemA  49551  precofvalALT  50296