Theorem ad3antlr 727

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 722	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  772  disjxiun  5144  fimaproj  8123  tfrlem1  8378  oaass  8563  undomOLD  9062  acndom2  10051  infxp  10212  isf32lem2  10351  ttukeylem3  10508  gchina  10696  r1limwun  10733  difreicc  13465  ssfzo12bi  13731  flflp1  13776  hasheqf1oi  14315  ccatcl  14528  cshwidxmodr  14758  wwlktovf1  14912  o1of2  15561  rlimsqzlem  15599  lcmgcdlem  16547  isprm5  16648  ramval  16945  mreexexlem4d  17595  acsfn  17607  gsumpropd2lem  18604  issubmgm2  18628  gasubg  19207  psgndiflemB  21372  psgndiflemA  21373  psrass1  21744  mdetf  22317  cpmatacl  22438  cpmatinvcl  22439  mat2pmatf1  22451  mp2pm2mplem4  22531  chfacffsupp  22578  restcld  22896  cnpnei  22988  iscncl  22993  cncls  22998  cnntr  22999  1stcfb  23169  2ndcdisj  23180  txlly  23360  fbflim  23700  fclsbas  23745  nmoi  24465  mpomulcn  24605  fgcfil  25019  equivcau  25048  cmetcusp  25102  itg2cnlem1  25511  iblss  25554  lgsqr  27090  lgsqrmodndvds  27092  noetainflem4  27479  slerec  27557  axcontlem2  28490  nbuhgr  28867  nbusgrvtxm1  28903  2pthon3v  29464  clwwisshclwwslem  29534  wwlksext2clwwlk  29577  2pthfrgr  29804  vdgn1frgrv2  29816  frgrwopreg  29843  numclwlk2lem2f1o  29899  blocnilem  30324  mdslmd3i  31852  foresf1o  32009  2ndresdju  32141  fgreu  32164  fdifsuppconst  32178  resf1o  32222  omndmul2  32500  psgnfzto1st  32534  isdrng4  32665  nsgqusf1olem3  32800  elrspunidl  32820  elrspunsn  32821  qsidomlem1  32845  lbsdiflsp0  32999  evls1fldgencl  33033  ist0cld  33111  locfinreflem  33118  cmpcref  33128  zarclsun  33148  pstmxmet  33175  lmdvg  33231  carsgclctunlem3  33617  oddpwdc  33651  sgnmul  33839  signstres  33884  tgoldbachgtd  33972  cvmlift2lem12  34603  satfdmlem  34657  satffunlem2lem1  34693  mrsubff  34801  elicc3  35505  nn0prpwlem  35510  neibastop2  35549  neibastop3  35550  bj-prmoore  36299  ltflcei  36779  matunitlindflem2  36788  poimirlem4  36795  poimirlem13  36804  poimirlem14  36805  poimirlem26  36817  poimirlem27  36818  poimirlem28  36819  poimirlem29  36820  poimirlem31  36822  heicant  36826  mblfinlem2  36829  mblfinlem3  36830  mblfinlem4  36831  ismblfin  36832  itg2addnclem  36842  itg2addnclem2  36843  itg2addnclem3  36844  itg2addnc  36845  itg2gt0cn  36846  ftc1cnnc  36863  ftc1anclem5  36868  ftc1anclem6  36869  ftc1anclem7  36870  ftc1anclem8  36871  ftc1anc  36872  nnubfi  36921  nninfnub  36922  linepsubN  38926  lhpmatb  39205  cdlemf2  39736  diaglbN  40229  diaintclN  40232  dibglbN  40340  dibintclN  40341  dihlsscpre  40408  dihglblem5aN  40466  dihglblem2aN  40467  dih1dimatlem  40503  sticksstones12a  41279  fsuppind  41464  diophren  41853  irrapxlem2  41863  irrapxlem4  41865  wepwsolem  42086  omlimcl2  42293  tfsconcatfv  42393  ofoafg  42406  prmunb2  43372  cvgdvgrat  43374  fiiuncl  44053  infleinflem2  44379  supxrunb3  44407  supminfxr  44472  limsuppnflem  44724  limsupmnflem  44734  limsupre3lem  44746  dfxlim2v  44861  icccncfext  44901  ioodvbdlimc1lem1  44945  iblcncfioo  44992  wallispilem3  45081  fourierdlem12  45133  fourierdlem34  45155  fourierdlem50  45170  fourierdlem51  45171  fourierdlem65  45185  fourierdlem77  45197  meaiuninc3v  45498  hoicvr  45562  hspdifhsp  45630  smflimlem4  45788  iccpartigtl  46389  iccpartgt  46393  fargshiftfva  46409  sfprmdvdsmersenne  46569  opoeALTV  46649  opeoALTV  46650  nnsum4primeseven  46766  nnsum4primesevenALTV  46767  isomushgr  46792  isomuspgr  46800  uzlidlring  46915  2zrngmmgm  46932  cznrng  46941  ply1mulgsumlem2  47155  snlindsntor  47239  elbigo2  47325  nn0sumshdiglemA  47392