Theorem ad3antlr 767

Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad3antlr	⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem ad3antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	ad2antlr 763	. 2 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)
3	2	adantr 481	1 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  ad4antlr  769  disjxiun  4649  tfrlem1  7472  oaass  7641  undom  8048  acndom2  8877  infxp  9037  isf32lem2  9176  ttukeylem3  9333  gchina  9521  r1limwun  9558  difreicc  12304  ssfzo12bi  12563  flflp1  12608  hasheqf1oi  13140  ccatcl  13359  cshwidxmodr  13550  wwlktovf1  13700  o1of2  14343  rlimsqzlem  14379  lcmgcdlem  15319  isprm5  15419  ramval  15712  mreexexlem4d  16307  acsfn  16320  gsumpropd2lem  17273  gasubg  17735  psgndiflemB  19946  psgndiflemA  19947  mdetf  20401  cpmatacl  20521  cpmatinvcl  20522  mat2pmatf1  20534  mp2pm2mplem4  20614  chfacffsupp  20661  restcld  20976  cnpnei  21068  iscncl  21073  cncls  21078  cnntr  21079  1stcfb  21248  2ndcdisj  21259  txlly  21439  fbflim  21780  fclsbas  21825  nmoi  22532  fgcfil  23069  equivcau  23098  cmetcusp  23150  itg2cnlem1  23528  iblss  23571  lgsqr  25076  lgsqrmodndvds  25078  axcontlem2  25845  nbuhgr  26239  nbusgrvtxm1  26281  2pthon3v  26839  wwlksext2clwwlk  26924  clwwisshclwwslem  26927  2pthfrgr  27148  vdgn1frgrv2  27160  frgrwopreg  27187  numclwlk1lem2f1  27227  numclwlk2lem2f1o  27238  blocnilem  27659  mdslmd3i  29191  foresf1o  29343  fgreu  29471  resf1o  29505  omndmul2  29712  psgnfzto1st  29855  fimaproj  29900  locfinreflem  29907  cmpcref  29917  pstmxmet  29940  lmdvg  29999  carsgclctunlem3  30382  oddpwdc  30416  sgnmul  30604  signstres  30652  tgoldbachgtd  30740  cvmlift2lem12  31296  mrsubff  31409  slerec  31923  elicc3  32311  nn0prpwlem  32317  neibastop2  32356  neibastop3  32357  ltflcei  33397  matunitlindflem2  33406  poimirlem4  33413  poimirlem13  33422  poimirlem14  33423  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  poimirlem29  33438  poimirlem31  33440  heicant  33444  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  itg2addnclem  33461  itg2addnclem2  33462  itg2addnclem3  33463  itg2addnc  33464  itg2gt0cn  33465  ftc1cnnc  33484  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  nnubfi  33546  nninfnub  33547  linepsubN  35038  lhpmatb  35317  cdlemf2  35850  diaglbN  36344  diaintclN  36347  dibglbN  36455  dibintclN  36456  dihlsscpre  36523  dihglblem5aN  36581  dihglblem2aN  36582  dih1dimatlem  36618  diophren  37377  irrapxlem2  37387  irrapxlem4  37389  wepwsolem  37612  prmunb2  38510  cvgdvgrat  38512  fiiuncl  39234  infleinflem2  39587  supxrunb3  39623  supminfxr  39694  limsuppnflem  39942  limsupmnflem  39952  limsupre3lem  39964  dfxlim2v  40073  icccncfext  40100  ioodvbdlimc1lem1  40146  iblcncfioo  40194  wallispilem3  40284  fourierdlem12  40336  fourierdlem34  40358  fourierdlem50  40373  fourierdlem51  40374  fourierdlem65  40388  fourierdlem77  40400  hoicvr  40762  hspdifhsp  40830  smflimlem4  40982  iccpartigtl  41359  iccpartgt  41363  fargshiftfva  41379  sfprmdvdsmersenne  41520  opoeALTV  41594  opeoALTV  41595  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  issubmgm2  41790  uzlidlring  41929  2zrngmmgm  41946  cznrng  41955  ply1mulgsumlem2  42175  snlindsntor  42260  elbigo2  42346  nn0sumshdiglemA  42413