Theorem ad3antlr 730

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  simpllr  775  disjxiun  5163  fimaproj  8176  tfrlem1  8432  oaass  8617  undomOLD  9126  acndom2  10123  infxp  10283  isf32lem2  10423  ttukeylem3  10580  gchina  10768  r1limwun  10805  difreicc  13544  ssfzo12bi  13811  flflp1  13858  hasheqf1oi  14400  ccatcl  14622  cshwidxmodr  14852  wwlktovf1  15006  o1of2  15659  rlimsqzlem  15697  lcmgcdlem  16653  isprm5  16754  ramval  17055  mreexexlem4d  17705  acsfn  17717  gsumpropd2lem  18717  issubmgm2  18741  gasubg  19342  psgndiflemB  21641  psgndiflemA  21642  psrass1  22007  mhpmulcl  22176  mdetf  22622  cpmatacl  22743  cpmatinvcl  22744  mat2pmatf1  22756  mp2pm2mplem4  22836  chfacffsupp  22883  restcld  23201  cnpnei  23293  iscncl  23298  cncls  23303  cnntr  23304  1stcfb  23474  2ndcdisj  23485  txlly  23665  fbflim  24005  fclsbas  24050  nmoi  24770  mpomulcn  24910  fgcfil  25324  equivcau  25353  cmetcusp  25407  itg2cnlem1  25816  iblss  25860  lgsqr  27413  lgsqrmodndvds  27415  noetainflem4  27803  slerec  27882  remulscllem2  28451  axcontlem2  28998  nbuhgr  29378  nbusgrvtxm1  29414  2pthon3v  29976  clwwisshclwwslem  30046  wwlksext2clwwlk  30089  2pthfrgr  30316  vdgn1frgrv2  30328  frgrwopreg  30355  numclwlk2lem2f1o  30411  blocnilem  30836  mdslmd3i  32364  foresf1o  32532  2ndresdju  32667  fgreu  32690  fdifsuppconst  32701  resf1o  32744  chnso  32986  omndmul2  33062  psgnfzto1st  33098  isdrng4  33264  nsgqusf1olem3  33408  elrspunidl  33421  elrspunsn  33422  qsidomlem1  33445  1arithidom  33530  dfufd2lem  33542  lbsdiflsp0  33639  evls1fldgencl  33680  ist0cld  33779  locfinreflem  33786  cmpcref  33796  zarclsun  33816  pstmxmet  33843  lmdvg  33899  carsgclctunlem3  34285  oddpwdc  34319  sgnmul  34507  signstres  34552  tgoldbachgtd  34639  cvmlift2lem12  35282  satfdmlem  35336  satffunlem2lem1  35372  mrsubff  35480  elicc3  36283  nn0prpwlem  36288  neibastop2  36327  neibastop3  36328  bj-prmoore  37081  ltflcei  37568  matunitlindflem2  37577  poimirlem4  37584  poimirlem13  37593  poimirlem14  37594  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  poimirlem29  37609  poimirlem31  37611  heicant  37615  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  itg2addnclem  37631  itg2addnclem2  37632  itg2addnclem3  37633  itg2addnc  37634  itg2gt0cn  37635  ftc1cnnc  37652  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  nnubfi  37710  nninfnub  37711  linepsubN  39709  lhpmatb  39988  cdlemf2  40519  diaglbN  41012  diaintclN  41015  dibglbN  41123  dibintclN  41124  dihlsscpre  41191  dihglblem5aN  41249  dihglblem2aN  41250  dih1dimatlem  41286  sticksstones12a  42114  fsuppind  42545  diophren  42769  irrapxlem2  42779  irrapxlem4  42781  wepwsolem  42999  omlimcl2  43203  tfsconcatfv  43303  ofoafg  43316  prmunb2  44280  cvgdvgrat  44282  fiiuncl  44967  infleinflem2  45286  supxrunb3  45314  supminfxr  45379  limsuppnflem  45631  limsupmnflem  45641  limsupre3lem  45653  dfxlim2v  45768  icccncfext  45808  ioodvbdlimc1lem1  45852  iblcncfioo  45899  wallispilem3  45988  fourierdlem12  46040  fourierdlem34  46062  fourierdlem50  46077  fourierdlem51  46078  fourierdlem65  46092  fourierdlem77  46104  meaiuninc3v  46405  hoicvr  46469  hspdifhsp  46537  smflimlem4  46695  iccpartigtl  47297  iccpartgt  47301  fargshiftfva  47317  sfprmdvdsmersenne  47477  opoeALTV  47557  opeoALTV  47558  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  isuspgrimlem  47758  gricushgr  47770  uspgrlimlem4  47815  uzlidlring  47958  2zrngmmgm  47975  cznrng  47984  ply1mulgsumlem2  48116  snlindsntor  48200  elbigo2  48286  nn0sumshdiglemA  48353