Theorem ad3antlr 731

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 726	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  5086  fimaproj  8065  tfrlem1  8295  oaass  8476  acndom2  9945  infxp  10105  isf32lem2  10245  ttukeylem3  10402  gchina  10590  r1limwun  10627  difreicc  13384  ssfzo12bi  13661  flflp1  13711  hasheqf1oi  14258  ccatcl  14481  cshwidxmodr  14711  wwlktovf1  14864  o1of2  15520  rlimsqzlem  15556  lcmgcdlem  16517  isprm5  16618  ramval  16920  mreexexlem4d  17553  acsfn  17565  chnso  18530  gsumpropd2lem  18587  issubmgm2  18611  gasubg  19214  omndmul2  20045  psgndiflemB  21537  psgndiflemA  21538  psrass1  21901  mhpmulcl  22064  mdetf  22510  cpmatacl  22631  cpmatinvcl  22632  mat2pmatf1  22644  mp2pm2mplem4  22724  chfacffsupp  22771  restcld  23087  cnpnei  23179  iscncl  23184  cncls  23189  cnntr  23190  1stcfb  23360  2ndcdisj  23371  txlly  23551  fbflim  23891  fclsbas  23936  nmoi  24643  mpomulcn  24785  fgcfil  25198  equivcau  25227  cmetcusp  25281  itg2cnlem1  25689  iblss  25733  lgsqr  27289  lgsqrmodndvds  27291  noetainflem4  27679  slerec  27760  remulscllem2  28403  axcontlem2  28943  nbuhgr  29321  nbusgrvtxm1  29357  2pthon3v  29921  clwwisshclwwslem  29994  wwlksext2clwwlk  30037  2pthfrgr  30264  vdgn1frgrv2  30276  frgrwopreg  30303  numclwlk2lem2f1o  30359  blocnilem  30784  mdslmd3i  32312  foresf1o  32484  2ndresdju  32631  fgreu  32654  fdifsuppconst  32670  resf1o  32713  sgnmul  32818  psgnfzto1st  33074  elrgspnsubrunlem1  33214  isdrng4  33261  nsgqusf1olem3  33380  elrspunidl  33393  elrspunsn  33394  qsidomlem1  33417  1arithidom  33502  dfufd2lem  33514  mplvrpmga  33575  lbsdiflsp0  33639  evls1fldgencl  33683  cos9thpiminplylem2  33796  ist0cld  33846  locfinreflem  33853  cmpcref  33863  zarclsun  33883  pstmxmet  33910  lmdvg  33966  carsgclctunlem3  34333  oddpwdc  34367  signstres  34588  tgoldbachgtd  34675  cvmlift2lem12  35358  satfdmlem  35412  satffunlem2lem1  35448  mrsubff  35556  elicc3  36361  nn0prpwlem  36366  neibastop2  36405  neibastop3  36406  bj-prmoore  37159  ltflcei  37647  matunitlindflem2  37656  poimirlem4  37663  poimirlem13  37672  poimirlem14  37673  poimirlem26  37685  poimirlem27  37686  poimirlem28  37687  poimirlem29  37688  poimirlem31  37690  heicant  37694  mblfinlem2  37697  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  itg2addnclem  37710  itg2addnclem2  37711  itg2addnclem3  37712  itg2addnc  37713  itg2gt0cn  37714  ftc1cnnc  37731  ftc1anclem5  37736  ftc1anclem6  37737  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  nnubfi  37789  nninfnub  37790  linepsubN  39850  lhpmatb  40129  cdlemf2  40660  diaglbN  41153  diaintclN  41156  dibglbN  41264  dibintclN  41265  dihlsscpre  41332  dihglblem5aN  41390  dihglblem2aN  41391  dih1dimatlem  41427  sticksstones12a  42249  fsuppind  42682  diophren  42905  irrapxlem2  42915  irrapxlem4  42917  wepwsolem  43134  omlimcl2  43334  tfsconcatfv  43433  ofoafg  43446  prmunb2  44403  cvgdvgrat  44405  fiiuncl  45161  infleinflem2  45468  supxrunb3  45496  supminfxr  45561  limsuppnflem  45807  limsupmnflem  45817  limsupre3lem  45829  dfxlim2v  45944  icccncfext  45984  ioodvbdlimc1lem1  46028  iblcncfioo  46075  wallispilem3  46164  fourierdlem12  46216  fourierdlem34  46238  fourierdlem50  46253  fourierdlem51  46254  fourierdlem65  46268  fourierdlem77  46280  meaiuninc3v  46581  hoicvr  46645  hspdifhsp  46713  smflimlem4  46871  iccpartigtl  47522  iccpartgt  47526  fargshiftfva  47542  sfprmdvdsmersenne  47702  opoeALTV  47782  opeoALTV  47783  nnsum4primeseven  47899  nnsum4primesevenALTV  47900  uhgrimedgi  47989  isuspgrimlem  47994  gricushgr  48016  isubgr3stgrlem7  48071  uspgrlimlem4  48090  gpgedgvtx1  48161  pgn4cyclex  48225  uzlidlring  48334  2zrngmmgm  48351  cznrng  48360  ply1mulgsumlem2  48487  snlindsntor  48571  elbigo2  48652  nn0sumshdiglemA  48719  precofvalALT  49468