Theorem ad2antlr 480

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad2antlr	⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)

Proof of Theorem ad2antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 274	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantll 467	1 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad3antlr  484  simplr  519  simplrl  524  simplrr  525  ordtri2or2exmidlem  4441  en2lp  4469  foun  5386  f1oprg  5411  fcof1o  5690  foeqcnvco  5691  f1eqcocnv  5692  caovord3  5944  f1o2ndf1  6125  smores2  6191  frecrdg  6305  nnaordex  6423  xpdom2  6725  xpen  6739  mapen  6740  xpmapenlem  6743  nndomo  6758  phpm  6759  fidifsnen  6764  isinfinf  6791  finexdc  6796  fientri3  6803  fiintim  6817  xpfi  6818  f1dmvrnfibi  6832  sbthlemi8  6852  djudom  6978  omp1eomlem  6979  difinfsn  6985  ctmlemr  6993  ctssdccl  6996  enomnilem  7010  finomni  7012  ismkvnex  7029  exmidfodomrlemrALT  7059  dfplpq2  7162  recclnq  7200  subhalfnqq  7222  distrnq0  7267  prarloclem3step  7304  genpml  7325  genpmu  7326  addnqprl  7337  addnqpru  7338  appdivnq  7371  mulnqprl  7376  mulnqpru  7377  mullocpr  7379  ltexprlemfl  7417  ltexprlemfu  7419  ltmprr  7450  archpr  7451  cauappcvgprlemm  7453  caucvgprlemladdrl  7486  caucvgprprlemopl  7505  caucvgprprlemopu  7507  recexgt0sr  7581  mulgt0sr  7586  elrealeu  7637  axcaucvglemcau  7706  axcaucvglemres  7707  cnegex  7940  apirr  8367  mulge0  8381  lemul12a  8620  lediv2a  8653  creur  8717  nndiv  8761  zaddcllemneg  9093  peano5uzti  9159  supinfneg  9390  infsupneg  9391  divfnzn  9413  xrltso  9582  xpncan  9654  xltadd1  9659  xleaddadd  9670  elioc2  9719  elico2  9720  elicc2  9721  exfzdc  10017  exbtwnzlemex  10027  rebtwn2z  10032  modqid  10122  modqcyc  10132  mulqaddmodid  10137  modqadd2mod  10147  addmodlteq  10171  frecuzrdgg  10189  seq3val  10231  seqvalcd  10232  seq3clss  10240  iseqf1olemqcl  10259  iseqf1olemnab  10261  seq3f1olemp  10275  seq3f1o  10277  fser0const  10289  ser3ge0  10290  exp3vallem  10294  facndiv  10485  faclbnd  10487  bcval5  10509  hashen  10530  fihashdom  10549  hashunlem  10550  hashfacen  10579  zfz1isolemiso  10582  seq3coll  10585  caucvgre  10753  resqrexlemlo  10785  cau3lem  10886  qdenre  10974  rexico  10993  fimaxre2  10998  xrmaxiflemcl  11014  xrmaxifle  11015  xrmaxiflemcom  11018  2clim  11070  cn1lem  11083  climsqz  11104  climsqz2  11105  climcau  11116  sumrbdclem  11146  summodclem2a  11150  fsum3  11156  fsumcl2lem  11167  fsumadd  11175  sumsnf  11178  fsum2dlemstep  11203  fisum0diag2  11216  fsummulc2  11217  mertenslemub  11303  mertenslemi1  11304  mertensabs  11306  ntrivcvgap  11317  prodrbdclem  11340  prodmodclem3  11344  prodmodclem2a  11345  prodmodc  11347  efaddlem  11380  tanaddaplem  11445  zdvdsdc  11514  dvdseq  11546  dvdsext  11553  odd2np1  11570  sqoddm1div8z  11583  nno  11603  zsupcllemstep  11638  infssuzex  11642  dfgcd3  11698  dvdslcm  11750  lcmneg  11755  lcmgcdlem  11758  ncoprmgcdne1b  11770  qredeq  11777  qredeu  11778  divgcdcoprm0  11782  exprmfct  11818  prmdvdsfz  11819  rpexp1i  11832  sqrt2irr  11840  nonsq  11885  ctinfom  11941  enctlem  11945  setsfun  11994  setsfun0  11995  setscom  11999  tgdom  12241  ssrest  12351  cnfval  12363  cnpfval  12364  cnpval  12367  iscnp3  12372  ssidcn  12379  cnpnei  12388  cnntr  12394  cncnp  12399  cnptopresti  12407  tx1cn  12438  upxp  12441  imasnopn  12468  bdmet  12671  metcnp  12681  ivthinclemlr  12784  ivthinclemur  12786  ivthinc  12790  dvrecap  12846  pilem3  12864  nnsf  13199  peano4nninf  13200  nninfalllemn  13202  nninfalllem1  13203  nninfsellemqall  13211  nninfsellemeqinf  13212  nninffeq  13216  exmidsbthrlem  13217