Theorem ad2antlr 476

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  ad3antlr  480  simplr  500  simplrl  505  simplrr  506  ordtri2or2exmidlem  4379  en2lp  4407  foun  5320  f1oprg  5343  fcof1o  5622  foeqcnvco  5623  f1eqcocnv  5624  caovord3  5876  f1o2ndf1  6055  smores2  6121  frecrdg  6235  nnaordex  6353  xpdom2  6654  xpen  6668  mapen  6669  xpmapenlem  6672  nndomo  6687  phpm  6688  fidifsnen  6693  isinfinf  6720  finexdc  6725  fientri3  6732  fiintim  6746  xpfi  6747  f1dmvrnfibi  6760  sbthlemi8  6780  djudom  6893  omp1eomlem  6894  difinfsn  6900  ctmlemr  6908  ctssdclemr  6911  enomnilem  6922  finomni  6924  exmidfodomrlemrALT  6968  dfplpq2  7063  recclnq  7101  subhalfnqq  7123  distrnq0  7168  prarloclem3step  7205  genpml  7226  genpmu  7227  addnqprl  7238  addnqpru  7239  appdivnq  7272  mulnqprl  7277  mulnqpru  7278  mullocpr  7280  ltexprlemfl  7318  ltexprlemfu  7320  ltmprr  7351  archpr  7352  cauappcvgprlemm  7354  caucvgprlemladdrl  7387  caucvgprprlemopl  7406  caucvgprprlemopu  7408  recexgt0sr  7469  mulgt0sr  7473  elrealeu  7517  axcaucvglemcau  7583  axcaucvglemres  7584  cnegex  7811  apirr  8233  mulge0  8247  lemul12a  8478  lediv2a  8511  creur  8575  nndiv  8619  zaddcllemneg  8945  peano5uzti  9011  supinfneg  9240  infsupneg  9241  divfnzn  9263  xrltso  9423  xpncan  9495  xltadd1  9500  xleaddadd  9511  elioc2  9560  elico2  9561  elicc2  9562  exfzdc  9858  exbtwnzlemex  9868  rebtwn2z  9873  modqid  9963  modqcyc  9973  mulqaddmodid  9978  modqadd2mod  9988  addmodlteq  10012  frecuzrdgg  10030  seq3val  10072  seqvalcd  10073  seq3clss  10081  iseqf1olemqcl  10100  iseqf1olemnab  10102  seq3f1olemp  10116  seq3f1o  10118  fser0const  10130  ser3ge0  10131  exp3vallem  10135  facndiv  10326  faclbnd  10328  bcval5  10350  hashen  10371  fihashdom  10390  hashunlem  10391  hashfacen  10420  zfz1isolemiso  10423  seq3coll  10426  caucvgre  10593  resqrexlemlo  10625  cau3lem  10726  qdenre  10814  rexico  10833  fimaxre2  10837  xrmaxiflemcl  10853  xrmaxifle  10854  xrmaxiflemcom  10857  2clim  10909  cn1lem  10922  climsqz  10943  climsqz2  10944  climcau  10955  sumrbdclem  10984  summodclem2a  10989  fsum3  10995  fsumcl2lem  11006  fsumadd  11014  sumsnf  11017  fsum2dlemstep  11042  fisum0diag2  11055  fsummulc2  11056  mertenslemub  11142  mertenslemi1  11143  mertensabs  11145  efaddlem  11178  tanaddaplem  11243  zdvdsdc  11309  dvdseq  11341  dvdsext  11348  odd2np1  11365  sqoddm1div8z  11378  nno  11398  zsupcllemstep  11433  infssuzex  11437  dfgcd3  11491  dvdslcm  11543  lcmneg  11548  lcmgcdlem  11551  ncoprmgcdne1b  11563  qredeq  11570  qredeu  11571  divgcdcoprm0  11575  exprmfct  11611  prmdvdsfz  11612  rpexp1i  11625  sqrt2irr  11633  nonsq  11677  ctinfom  11733  setsfun  11776  setsfun0  11777  setscom  11781  tgdom  12023  ssrest  12133  cnfval  12145  cnpfval  12146  cnpval  12148  iscnp3  12153  ssidcn  12160  cnpnei  12169  cnntr  12175  cncnp  12180  cnptopresti  12188  tx1cn  12219  upxp  12222  imasnopn  12249  bdmet  12430  metcnp  12436  nnsf  12783  peano4nninf  12784  nninfalllemn  12786  nninfalllem1  12787  nninfsellemqall  12795  nninfsellemeqinf  12796  nninffeq  12800  exmidsbthrlem  12801