Theorem ad2antlr 489

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 276	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantll 476	1 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  ad3antlr  493  simplr  528  simplrl  535  simplrr  536  ordtri2or2exmidlem  4543  en2lp  4571  foun  5499  f1oprg  5524  fcof1o  5811  foeqcnvco  5812  f1eqcocnv  5813  caovord3  6070  f1o2ndf1  6253  smores2  6319  frecrdg  6433  nnaordex  6553  xpdom2  6857  xpen  6873  mapen  6874  xpmapenlem  6877  nndomo  6892  phpm  6893  fidifsnen  6898  isinfinf  6925  finexdc  6930  fientri3  6943  fiintim  6957  xpfi  6958  f1dmvrnfibi  6973  sbthlemi8  6993  djudom  7122  omp1eomlem  7123  difinfsn  7129  ctmlemr  7137  ctssdccl  7140  nnnninfeq  7156  enomnilem  7166  finomni  7168  ismkvnex  7183  enmkvlem  7189  nninfwlpoimlemginf  7204  exmidfodomrlemrALT  7232  exmidontriim  7254  netap  7283  exmidapne  7289  dfplpq2  7383  recclnq  7421  subhalfnqq  7443  distrnq0  7488  prarloclem3step  7525  genpml  7546  genpmu  7547  addnqprl  7558  addnqpru  7559  appdivnq  7592  mulnqprl  7597  mulnqpru  7598  mullocpr  7600  ltexprlemfl  7638  ltexprlemfu  7640  ltmprr  7671  archpr  7672  cauappcvgprlemm  7674  caucvgprlemladdrl  7707  caucvgprprlemopl  7726  caucvgprprlemopu  7728  recexgt0sr  7802  mulgt0sr  7807  elrealeu  7858  axcaucvglemcau  7927  axcaucvglemres  7928  cnegex  8165  apirr  8592  mulge0  8606  lemul12a  8849  lediv2a  8882  creur  8946  nndiv  8990  zaddcllemneg  9322  peano5uzti  9391  supinfneg  9625  infsupneg  9626  divfnzn  9651  xrltso  9826  xpncan  9901  xltadd1  9906  xleaddadd  9917  elioc2  9966  elico2  9967  elicc2  9968  exfzdc  10270  exbtwnzlemex  10280  rebtwn2z  10285  modqid  10380  modqcyc  10390  mulqaddmodid  10395  modqadd2mod  10405  addmodlteq  10429  frecuzrdgg  10447  seq3val  10489  seqvalcd  10490  seq3clss  10498  iseqf1olemqcl  10517  iseqf1olemnab  10519  seq3f1olemp  10533  seq3f1o  10535  fser0const  10547  ser3ge0  10548  exp3vallem  10552  qsqeqor  10662  facndiv  10751  faclbnd  10753  bcval5  10775  hashen  10796  fihashdom  10815  hashunlem  10816  hashfacen  10848  zfz1isolemiso  10851  seq3coll  10854  caucvgre  11022  resqrexlemlo  11054  cau3lem  11155  qdenre  11243  rexico  11262  fimaxre2  11267  2zinfmin  11283  xrmaxiflemcl  11285  xrmaxifle  11286  xrmaxiflemcom  11289  2clim  11341  cn1lem  11354  climsqz  11375  climsqz2  11376  climcau  11387  sumrbdclem  11417  summodclem2a  11421  fsum3  11427  fsumcl2lem  11438  fsumadd  11446  sumsnf  11449  fsum2dlemstep  11474  fisum0diag2  11487  fsummulc2  11488  mertenslemub  11574  mertenslemi1  11575  mertensabs  11577  ntrivcvgap  11588  prodrbdclem  11611  prodmodclem3  11615  prodmodclem2a  11616  prodmodc  11618  prod1dc  11626  prodsnf  11632  fprod2dlemstep  11662  efaddlem  11714  tanaddaplem  11778  zdvdsdc  11851  dvdseq  11886  dvdsext  11893  odd2np1  11910  sqoddm1div8z  11923  nno  11943  zsupcllemstep  11978  infssuzex  11982  suprzubdc  11985  dfgcd3  12043  dvdslcm  12101  lcmneg  12106  lcmgcdlem  12109  ncoprmgcdne1b  12121  qredeq  12128  qredeu  12129  divgcdcoprm0  12133  exprmfct  12170  prmdvdsfz  12171  isprm5  12174  rpexp1i  12186  sqrt2irr  12194  nonsq  12239  eulerthlemrprm  12261  eulerthlema  12262  phisum  12272  modprmn0modprm0  12288  pclemdc  12320  pcz  12364  pcmpt  12375  fldivp1  12380  pcfac  12382  expnprm  12385  oddprmdvds  12386  prmpwdvds  12387  infpnlem1  12391  1arith  12399  4sqlem2  12421  4sqlemafi  12427  4sqleminfi  12429  4sqexercise2  12431  4sqlemsdc  12432  ctinfom  12479  enctlem  12483  nninfdclemlt  12502  setsfun  12547  setsfun0  12548  setscom  12552  mndissubm  12927  resmhm  12939  resmhm2  12940  mhmco  12942  dfgrp2  12971  isgrpinv  12998  mulgval  13064  mulgnnp1  13070  mulgz  13090  grpissubg  13133  resghm  13199  qusecsub  13268  isrng  13288  lmodfopne  13642  dflidl2rng  13797  mulgrhm2  13908  psrbaglesuppg  13950  tgdom  14029  ssrest  14139  cnfval  14151  cnpfval  14152  cnpval  14155  iscnp3  14160  ssidcn  14167  cnpnei  14176  cnntr  14182  cncnp  14187  cnptopresti  14195  tx1cn  14226  upxp  14229  imasnopn  14256  bdmet  14459  metcnp  14469  ivthinclemlr  14572  ivthinclemur  14574  ivthinc  14578  dvrecap  14634  pilem3  14661  relogeftb  14743  logbgcd1irr  14842  lgslem4  14862  lgsval  14863  lgsfvalg  14864  lgsval2lem  14869  lgsmod  14885  lgsdir2lem4  14890  lgsdinn0  14907  2sqlem6  14925  2sqlem7  14926  nnsf  15213  peano4nninf  15214  nninfalllem1  15216  nninfsellemqall  15223  nninfsellemeqinf  15224  nninffeq  15228  exmidsbthrlem  15229  isomninnlem  15237  iswomninnlem  15256  iswomni0  15258  ismkvnnlem  15259