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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  simpllr  775  disjxiun  5145  fimaproj  8118  tfrlem1  8373  oaass  8558  undomOLD  9057  acndom2  10046  infxp  10207  isf32lem2  10346  ttukeylem3  10503  gchina  10691  r1limwun  10728  difreicc  13458  ssfzo12bi  13724  flflp1  13769  hasheqf1oi  14308  ccatcl  14521  cshwidxmodr  14751  wwlktovf1  14905  o1of2  15554  rlimsqzlem  15592  lcmgcdlem  16540  isprm5  16641  ramval  16938  mreexexlem4d  17588  acsfn  17600  gsumpropd2lem  18595  gasubg  19161  psgndiflemB  21145  psgndiflemA  21146  psrass1  21517  mdetf  22089  cpmatacl  22210  cpmatinvcl  22211  mat2pmatf1  22223  mp2pm2mplem4  22303  chfacffsupp  22350  restcld  22668  cnpnei  22760  iscncl  22765  cncls  22770  cnntr  22771  1stcfb  22941  2ndcdisj  22952  txlly  23132  fbflim  23472  fclsbas  23517  nmoi  24237  fgcfil  24780  equivcau  24809  cmetcusp  24863  itg2cnlem1  25271  iblss  25314  lgsqr  26844  lgsqrmodndvds  26846  noetainflem4  27233  slerec  27310  axcontlem2  28213  nbuhgr  28590  nbusgrvtxm1  28626  2pthon3v  29187  clwwisshclwwslem  29257  wwlksext2clwwlk  29300  2pthfrgr  29527  vdgn1frgrv2  29539  frgrwopreg  29566  numclwlk2lem2f1o  29622  blocnilem  30045  mdslmd3i  31573  foresf1o  31730  2ndresdju  31862  fgreu  31885  fdifsuppconst  31899  resf1o  31943  omndmul2  32218  psgnfzto1st  32252  isdrng4  32384  nsgqusf1olem3  32515  elrspunidl  32535  elrspunsn  32536  qsidomlem1  32560  lbsdiflsp0  32700  ist0cld  32802  locfinreflem  32809  cmpcref  32819  zarclsun  32839  pstmxmet  32866  lmdvg  32922  carsgclctunlem3  33308  oddpwdc  33342  sgnmul  33530  signstres  33575  tgoldbachgtd  33663  cvmlift2lem12  34294  satfdmlem  34348  satffunlem2lem1  34384  mrsubff  34492  mpomulcn  35151  elicc3  35191  nn0prpwlem  35196  neibastop2  35235  neibastop3  35236  bj-prmoore  35985  ltflcei  36465  matunitlindflem2  36474  poimirlem4  36481  poimirlem13  36490  poimirlem14  36491  poimirlem26  36503  poimirlem27  36504  poimirlem28  36505  poimirlem29  36506  poimirlem31  36508  heicant  36512  mblfinlem2  36515  mblfinlem3  36516  mblfinlem4  36517  ismblfin  36518  itg2addnclem  36528  itg2addnclem2  36529  itg2addnclem3  36530  itg2addnc  36531  itg2gt0cn  36532  ftc1cnnc  36549  ftc1anclem5  36554  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  nnubfi  36607  nninfnub  36608  linepsubN  38612  lhpmatb  38891  cdlemf2  39422  diaglbN  39915  diaintclN  39918  dibglbN  40026  dibintclN  40027  dihlsscpre  40094  dihglblem5aN  40152  dihglblem2aN  40153  dih1dimatlem  40189  sticksstones12a  40962  fsuppind  41160  diophren  41537  irrapxlem2  41547  irrapxlem4  41549  wepwsolem  41770  omlimcl2  41977  tfsconcatfv  42077  ofoafg  42090  prmunb2  43056  cvgdvgrat  43058  fiiuncl  43738  infleinflem2  44068  supxrunb3  44096  supminfxr  44161  limsuppnflem  44413  limsupmnflem  44423  limsupre3lem  44435  dfxlim2v  44550  icccncfext  44590  ioodvbdlimc1lem1  44634  iblcncfioo  44681  wallispilem3  44770  fourierdlem12  44822  fourierdlem34  44844  fourierdlem50  44859  fourierdlem51  44860  fourierdlem65  44874  fourierdlem77  44886  meaiuninc3v  45187  hoicvr  45251  hspdifhsp  45319  smflimlem4  45477  iccpartigtl  46078  iccpartgt  46082  fargshiftfva  46098  sfprmdvdsmersenne  46258  opoeALTV  46338  opeoALTV  46339  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  isomushgr  46481  isomuspgr  46489  issubmgm2  46547  uzlidlring  46781  2zrngmmgm  46798  cznrng  46807  ply1mulgsumlem2  47022  snlindsntor  47106  elbigo2  47192  nn0sumshdiglemA  47259