Theorem ad3antlr 743

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  simpllr  787  disjxiun  5102  fimaproj  8119  tfrlem1  8350  oaass  8534  acndom2  10026  infxp  10185  isf32lem2  10326  ttukeylem3  10483  gchina  10672  r1limwun  10709  difreicc  13502  ssfzo12bi  13781  flflp1  13831  hasheqf1oi  14378  ccatcl  14601  cshwidxmodr  14831  wwlktovf1  14984  sgnmul  15134  o1of2  15654  rlimsqzlem  15690  lcmgcdlem  16654  isprm5  16756  ramval  17058  mreexexlem4d  17693  acsfn  17705  chnso  18670  gsumpropd2lem  18727  issubmgm2  18751  gasubg  19363  omndmul2  20194  unichnlidl  21331  qsidomlem1  21440  psgndiflemB  21710  psgndiflemA  21711  psrass1  22073  mhpmulcl  22272  mdetf  22713  cpmatacl  22834  cpmatinvcl  22835  mat2pmatf1  22847  mp2pm2mplem4  22927  chfacffsupp  22974  restcld  23290  cnpnei  23382  iscncl  23387  cncls  23392  cnntr  23393  1stcfb  23563  2ndcdisj  23574  txlly  23754  fbflim  24094  fclsbas  24139  nmoi  24846  mpomulcn  24987  fgcfil  25391  equivcau  25420  cmetcusp  25474  itg2cnlem1  25881  iblss  25925  lgsqr  27473  lgsqrmodndvds  27475  noetainflem4  27862  lesrec  27950  remulscllem2  28652  axcontlem2  29224  nbuhgr  29602  nbusgrvtxm1  29638  2pthon3v  30201  clwwisshclwwslem  30274  wwlksext2clwwlk  30317  2pthfrgr  30544  vdgn1frgrv2  30556  frgrwopreg  30583  numclwlk2lem2f1o  30639  blocnilem  31065  mdslmd3i  32593  foresf1o  32760  2ndresdju  32906  fgreu  32928  fdifsuppconst  32946  resf1o  32987  psgnfzto1st  33338  elrgspnsubrunlem1  33480  isdrng4  33531  nsgqusf1olem3  33640  elrspunidl  33652  elrspunsn  33653  dflringlem3  33703  dflring4  33705  1arithidom  33744  dfufd2lem  33756  mplvrpmga  33852  lbsdiflsp0  33933  evls1fldgencl  33977  cos9thpiminplylem2  34090  ist0cld  34140  locfinreflem  34147  cmpcref  34157  zarclsun  34177  pstmxmet  34204  lmdvg  34260  carsgclctunlem3  34627  oddpwdc  34661  signstres  34879  tgoldbachgtd  34966  cvmlift2lem12  35677  satfdmlem  35731  satffunlem2lem1  35767  mrsubff  35875  elicc3  36690  nn0prpwlem  36695  neibastop2  36734  neibastop3  36735  bj-prmoore  37617  ltflcei  38119  matunitlindflem2  38128  poimirlem4  38135  poimirlem13  38144  poimirlem14  38145  poimirlem26  38157  poimirlem27  38158  poimirlem28  38159  poimirlem29  38160  poimirlem31  38162  heicant  38166  mblfinlem2  38169  mblfinlem3  38170  mblfinlem4  38171  ismblfin  38172  itg2addnclem  38182  itg2addnclem2  38183  itg2addnclem3  38184  itg2addnc  38185  itg2gt0cn  38186  ftc1cnnc  38203  ftc1anclem5  38208  ftc1anclem6  38209  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  nnubfi  38261  nninfnub  38262  linepsubN  40388  lhpmatb  40667  cdlemf2  41198  diaglbN  41691  diaintclN  41694  dibglbN  41802  dibintclN  41803  dihlsscpre  41870  dihglblem5aN  41928  dihglblem2aN  41929  dih1dimatlem  41965  sticksstones12a  42786  fsuppind  43184  diophren  43402  irrapxlem2  43412  irrapxlem4  43414  wepwsolem  43631  omlimcl2  43831  tfsconcatfv  43930  ofoafg  43943  prmunb2  44885  cvgdvgrat  44887  fiiuncl  45643  infleinflem2  45944  supxrunb3  45972  supminfxr  46036  limsuppnflem  46282  limsupmnflem  46292  limsupre3lem  46304  dfxlim2v  46419  icccncfext  46459  ioodvbdlimc1lem1  46503  iblcncfioo  46550  wallispilem3  46639  fourierdlem12  46691  fourierdlem34  46713  fourierdlem50  46728  fourierdlem51  46729  fourierdlem65  46743  fourierdlem77  46755  meaiuninc3v  47056  hspdifhsp  47188  smflimlem4  47346  iccpartigtl  48027  iccpartgt  48031  fargshiftfva  48047  sfprmdvdsmersenne  48210  opoeALTV  48303  opeoALTV  48304  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  uhgrimedgi  48510  isuspgrimlem  48515  gricushgr  48537  isubgr3stgrlem7  48592  uspgrlimlem4  48611  gpgedgvtx1  48682  pgn4cyclex  48746  uzlidlring  48855  2zrngmmgm  48872  cznrng  48881  ply1mulgsumlem2  49018  snlindsntor  49102  elbigo2  49183  nn0sumshdiglemA  49250  precofvalALT  49997