Theorem ad3antlr 728

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  simpllr  773  disjxiun  5072  fimaproj  7985  tfrlem1  8216  oaass  8401  undomOLD  8856  acndom2  9819  infxp  9980  isf32lem2  10119  ttukeylem3  10276  gchina  10464  r1limwun  10501  difreicc  13225  ssfzo12bi  13491  flflp1  13536  hasheqf1oi  14075  ccatcl  14286  cshwidxmodr  14526  wwlktovf1  14681  o1of2  15331  rlimsqzlem  15369  lcmgcdlem  16320  isprm5  16421  ramval  16718  mreexexlem4d  17365  acsfn  17377  gsumpropd2lem  18372  gasubg  18917  psgndiflemB  20814  psgndiflemA  20815  mdetf  21753  cpmatacl  21874  cpmatinvcl  21875  mat2pmatf1  21887  mp2pm2mplem4  21967  chfacffsupp  22014  restcld  22332  cnpnei  22424  iscncl  22429  cncls  22434  cnntr  22435  1stcfb  22605  2ndcdisj  22616  txlly  22796  fbflim  23136  fclsbas  23181  nmoi  23901  fgcfil  24444  equivcau  24473  cmetcusp  24527  itg2cnlem1  24935  iblss  24978  lgsqr  26508  lgsqrmodndvds  26510  axcontlem2  27342  nbuhgr  27719  nbusgrvtxm1  27755  2pthon3v  28317  clwwisshclwwslem  28387  wwlksext2clwwlk  28430  2pthfrgr  28657  vdgn1frgrv2  28669  frgrwopreg  28696  numclwlk2lem2f1o  28752  blocnilem  29175  mdslmd3i  30703  foresf1o  30859  2ndresdju  30995  fgreu  31018  fdifsuppconst  31032  resf1o  31074  omndmul2  31347  psgnfzto1st  31381  nsgqusf1olem3  31609  elrspunidl  31615  qsidomlem1  31637  lbsdiflsp0  31716  ist0cld  31792  locfinreflem  31799  cmpcref  31809  zarclsun  31829  pstmxmet  31856  lmdvg  31912  carsgclctunlem3  32296  oddpwdc  32330  sgnmul  32518  signstres  32563  tgoldbachgtd  32651  cvmlift2lem12  33285  satfdmlem  33339  satffunlem2lem1  33375  mrsubff  33483  noetainflem4  33952  slerec  34022  elicc3  34515  nn0prpwlem  34520  neibastop2  34559  neibastop3  34560  bj-prmoore  35295  ltflcei  35774  matunitlindflem2  35783  poimirlem4  35790  poimirlem13  35799  poimirlem14  35800  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  poimirlem29  35815  poimirlem31  35817  heicant  35821  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  itg2addnclem  35837  itg2addnclem2  35838  itg2addnclem3  35839  itg2addnc  35840  itg2gt0cn  35841  ftc1cnnc  35858  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  nnubfi  35917  nninfnub  35918  linepsubN  37773  lhpmatb  38052  cdlemf2  38583  diaglbN  39076  diaintclN  39079  dibglbN  39187  dibintclN  39188  dihlsscpre  39255  dihglblem5aN  39313  dihglblem2aN  39314  dih1dimatlem  39350  sticksstones12a  40120  fsuppind  40286  diophren  40642  irrapxlem2  40652  irrapxlem4  40654  wepwsolem  40874  prmunb2  41936  cvgdvgrat  41938  fiiuncl  42620  infleinflem2  42917  supxrunb3  42946  supminfxr  43011  limsuppnflem  43258  limsupmnflem  43268  limsupre3lem  43280  dfxlim2v  43395  icccncfext  43435  ioodvbdlimc1lem1  43479  iblcncfioo  43526  wallispilem3  43615  fourierdlem12  43667  fourierdlem34  43689  fourierdlem50  43704  fourierdlem51  43705  fourierdlem65  43719  fourierdlem77  43731  meaiuninc3v  44029  hoicvr  44093  hspdifhsp  44161  smflimlem4  44319  iccpartigtl  44886  iccpartgt  44890  fargshiftfva  44906  sfprmdvdsmersenne  45066  opoeALTV  45146  opeoALTV  45147  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  isomushgr  45289  isomuspgr  45297  issubmgm2  45355  uzlidlring  45498  2zrngmmgm  45515  cznrng  45524  ply1mulgsumlem2  45739  snlindsntor  45823  elbigo2  45909  nn0sumshdiglemA  45976