Theorem ad3antlr 739

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  simpllr  783  disjxiun  5091  fimaproj  8103  tfrlem1  8334  oaass  8518  acndom2  10000  infxp  10160  isf32lem2  10301  ttukeylem3  10458  gchina  10647  r1limwun  10684  difreicc  13478  ssfzo12bi  13757  flflp1  13807  hasheqf1oi  14354  ccatcl  14577  cshwidxmodr  14807  wwlktovf1  14960  o1of2  15616  rlimsqzlem  15652  lcmgcdlem  16616  isprm5  16718  ramval  17020  mreexexlem4d  17655  acsfn  17667  chnso  18632  gsumpropd2lem  18689  issubmgm2  18713  gasubg  19318  omndmul2  20149  psgndiflemB  21625  psgndiflemA  21626  psrass1  21988  mhpmulcl  22187  mdetf  22628  cpmatacl  22749  cpmatinvcl  22750  mat2pmatf1  22762  mp2pm2mplem4  22842  chfacffsupp  22889  restcld  23205  cnpnei  23297  iscncl  23302  cncls  23307  cnntr  23308  1stcfb  23478  2ndcdisj  23489  txlly  23669  fbflim  24009  fclsbas  24054  nmoi  24761  mpomulcn  24902  fgcfil  25306  equivcau  25335  cmetcusp  25389  itg2cnlem1  25796  iblss  25840  lgsqr  27385  lgsqrmodndvds  27387  noetainflem4  27774  lesrec  27862  remulscllem2  28564  axcontlem2  29105  nbuhgr  29483  nbusgrvtxm1  29519  2pthon3v  30082  clwwisshclwwslem  30155  wwlksext2clwwlk  30198  2pthfrgr  30425  vdgn1frgrv2  30437  frgrwopreg  30464  numclwlk2lem2f1o  30520  blocnilem  30946  mdslmd3i  32474  foresf1o  32645  2ndresdju  32794  fgreu  32816  fdifsuppconst  32834  resf1o  32875  sgnmul  32980  psgnfzto1st  33239  elrgspnsubrunlem1  33382  isdrng4  33436  nsgqusf1olem3  33555  elrspunidl  33568  elrspunsn  33569  qsidomlem1  33593  dflringlem3  33646  dflring4  33648  1arithidom  33687  dfufd2lem  33699  mplvrpmga  33796  lbsdiflsp0  33877  evls1fldgencl  33921  cos9thpiminplylem2  34034  ist0cld  34084  locfinreflem  34091  cmpcref  34101  zarclsun  34121  pstmxmet  34148  lmdvg  34204  carsgclctunlem3  34571  oddpwdc  34605  signstres  34826  tgoldbachgtd  34913  cvmlift2lem12  35612  satfdmlem  35666  satffunlem2lem1  35702  mrsubff  35810  elicc3  36625  nn0prpwlem  36630  neibastop2  36669  neibastop3  36670  bj-prmoore  37553  ltflcei  38055  matunitlindflem2  38064  poimirlem4  38071  poimirlem13  38080  poimirlem14  38081  poimirlem26  38093  poimirlem27  38094  poimirlem28  38095  poimirlem29  38096  poimirlem31  38098  heicant  38102  mblfinlem2  38105  mblfinlem3  38106  mblfinlem4  38107  ismblfin  38108  itg2addnclem  38118  itg2addnclem2  38119  itg2addnclem3  38120  itg2addnc  38121  itg2gt0cn  38122  ftc1cnnc  38139  ftc1anclem5  38144  ftc1anclem6  38145  ftc1anclem7  38146  ftc1anclem8  38147  ftc1anc  38148  nnubfi  38197  nninfnub  38198  linepsubN  40324  lhpmatb  40603  cdlemf2  41134  diaglbN  41627  diaintclN  41630  dibglbN  41738  dibintclN  41739  dihlsscpre  41806  dihglblem5aN  41864  dihglblem2aN  41865  dih1dimatlem  41901  sticksstones12a  42722  fsuppind  43120  diophren  43338  irrapxlem2  43348  irrapxlem4  43350  wepwsolem  43567  omlimcl2  43767  tfsconcatfv  43866  ofoafg  43879  prmunb2  44835  cvgdvgrat  44837  fiiuncl  45593  infleinflem2  45894  supxrunb3  45922  supminfxr  45986  limsuppnflem  46232  limsupmnflem  46242  limsupre3lem  46254  dfxlim2v  46369  icccncfext  46409  ioodvbdlimc1lem1  46453  iblcncfioo  46500  wallispilem3  46589  fourierdlem12  46641  fourierdlem34  46663  fourierdlem50  46678  fourierdlem51  46679  fourierdlem65  46693  fourierdlem77  46705  meaiuninc3v  47006  hspdifhsp  47138  smflimlem4  47296  iccpartigtl  47977  iccpartgt  47981  fargshiftfva  47997  sfprmdvdsmersenne  48160  opoeALTV  48253  opeoALTV  48254  nnsum4primeseven  48370  nnsum4primesevenALTV  48371  uhgrimedgi  48460  isuspgrimlem  48465  gricushgr  48487  isubgr3stgrlem7  48542  uspgrlimlem4  48561  gpgedgvtx1  48632  pgn4cyclex  48696  uzlidlring  48805  2zrngmmgm  48822  cznrng  48831  ply1mulgsumlem2  48957  snlindsntor  49041  elbigo2  49122  nn0sumshdiglemA  49189  precofvalALT  49937