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

This theorem is referenced by:  simpllr  775  disjxiun  5140  fimaproj  8135  tfrlem1  8391  oaass  8576  undomOLD  9079  acndom2  10072  infxp  10233  isf32lem2  10372  ttukeylem3  10529  gchina  10717  r1limwun  10754  difreicc  13488  ssfzo12bi  13754  flflp1  13799  hasheqf1oi  14337  ccatcl  14551  cshwidxmodr  14781  wwlktovf1  14935  o1of2  15584  rlimsqzlem  15622  lcmgcdlem  16571  isprm5  16672  ramval  16971  mreexexlem4d  17621  acsfn  17633  gsumpropd2lem  18633  issubmgm2  18657  gasubg  19247  psgndiflemB  21526  psgndiflemA  21527  psrass1  21901  mdetf  22491  cpmatacl  22612  cpmatinvcl  22613  mat2pmatf1  22625  mp2pm2mplem4  22705  chfacffsupp  22752  restcld  23070  cnpnei  23162  iscncl  23167  cncls  23172  cnntr  23173  1stcfb  23343  2ndcdisj  23354  txlly  23534  fbflim  23874  fclsbas  23919  nmoi  24639  mpomulcn  24779  fgcfil  25193  equivcau  25222  cmetcusp  25276  itg2cnlem1  25685  iblss  25728  lgsqr  27278  lgsqrmodndvds  27280  noetainflem4  27667  slerec  27746  remulscllem2  28223  axcontlem2  28770  nbuhgr  29150  nbusgrvtxm1  29186  2pthon3v  29748  clwwisshclwwslem  29818  wwlksext2clwwlk  29861  2pthfrgr  30088  vdgn1frgrv2  30100  frgrwopreg  30127  numclwlk2lem2f1o  30183  blocnilem  30608  mdslmd3i  32136  foresf1o  32294  2ndresdju  32429  fgreu  32452  fdifsuppconst  32464  resf1o  32507  omndmul2  32787  psgnfzto1st  32821  isdrng4  32957  nsgqusf1olem3  33120  elrspunidl  33139  elrspunsn  33140  qsidomlem1  33163  lbsdiflsp0  33315  evls1fldgencl  33349  ist0cld  33429  locfinreflem  33436  cmpcref  33446  zarclsun  33466  pstmxmet  33493  lmdvg  33549  carsgclctunlem3  33935  oddpwdc  33969  sgnmul  34157  signstres  34202  tgoldbachgtd  34289  cvmlift2lem12  34919  satfdmlem  34973  satffunlem2lem1  35009  mrsubff  35117  elicc3  35796  nn0prpwlem  35801  neibastop2  35840  neibastop3  35841  bj-prmoore  36589  ltflcei  37076  matunitlindflem2  37085  poimirlem4  37092  poimirlem13  37101  poimirlem14  37102  poimirlem26  37114  poimirlem27  37115  poimirlem28  37116  poimirlem29  37117  poimirlem31  37119  heicant  37123  mblfinlem2  37126  mblfinlem3  37127  mblfinlem4  37128  ismblfin  37129  itg2addnclem  37139  itg2addnclem2  37140  itg2addnclem3  37141  itg2addnc  37142  itg2gt0cn  37143  ftc1cnnc  37160  ftc1anclem5  37165  ftc1anclem6  37166  ftc1anclem7  37167  ftc1anclem8  37168  ftc1anc  37169  nnubfi  37218  nninfnub  37219  linepsubN  39220  lhpmatb  39499  cdlemf2  40030  diaglbN  40523  diaintclN  40526  dibglbN  40634  dibintclN  40635  dihlsscpre  40702  dihglblem5aN  40760  dihglblem2aN  40761  dih1dimatlem  40797  sticksstones12a  41624  fsuppind  41814  diophren  42224  irrapxlem2  42234  irrapxlem4  42236  wepwsolem  42457  omlimcl2  42661  tfsconcatfv  42761  ofoafg  42774  prmunb2  43739  cvgdvgrat  43741  fiiuncl  44420  infleinflem2  44744  supxrunb3  44772  supminfxr  44837  limsuppnflem  45089  limsupmnflem  45099  limsupre3lem  45111  dfxlim2v  45226  icccncfext  45266  ioodvbdlimc1lem1  45310  iblcncfioo  45357  wallispilem3  45446  fourierdlem12  45498  fourierdlem34  45520  fourierdlem50  45535  fourierdlem51  45536  fourierdlem65  45550  fourierdlem77  45562  meaiuninc3v  45863  hoicvr  45927  hspdifhsp  45995  smflimlem4  46153  iccpartigtl  46754  iccpartgt  46758  fargshiftfva  46774  sfprmdvdsmersenne  46934  opoeALTV  47014  opeoALTV  47015  nnsum4primeseven  47131  nnsum4primesevenALTV  47132  isuspgrimlem  47163  gricushgr  47174  uzlidlring  47288  2zrngmmgm  47305  cznrng  47314  ply1mulgsumlem2  47446  snlindsntor  47530  elbigo2  47616  nn0sumshdiglemA  47683