Theorem ad2antlr 472

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  ad3antlr  476  simplr  496  simplrl  501  simplrr  502  ordtri2or2exmidlem  4269  en2lp  4297  xpid11m  4575  foun  5165  f1oprg  5188  fcof1o  5449  foeqcnvco  5450  f1eqcocnv  5451  caovord3  5694  f1o2ndf1  5869  smores2  5932  frecrdg  6015  nnaordex  6123  xpdom2  6328  nndomo  6350  phpm  6351  fidifsnen  6355  fientri3  6381  f1dmvrnfibi  6393  dfplpq2  6544  recclnq  6582  subhalfnqq  6604  distrnq0  6649  prarloclem3step  6686  genpml  6707  genpmu  6708  addnqprl  6719  addnqpru  6720  appdivnq  6753  mulnqprl  6758  mulnqpru  6759  mullocpr  6761  ltexprlemfl  6799  ltexprlemfu  6801  ltmprr  6832  archpr  6833  cauappcvgprlemm  6835  caucvgprlemladdrl  6868  caucvgprprlemopl  6887  caucvgprprlemopu  6889  recexgt0sr  6950  mulgt0sr  6954  elrealeu  6998  axcaucvglemcau  7064  axcaucvglemres  7065  cnegex  7286  apirr  7705  mulge0  7719  lemul12a  7940  lediv2a  7973  creur  8036  nndiv  8079  zaddcllemneg  8390  peano5uzti  8455  supinfneg  8683  infsupneg  8684  divfnzn  8706  xrltso  8871  elioc2  8959  elico2  8960  elicc2  8961  exfzdc  9249  qbtwnzlemstep  9257  qbtwnzlemex  9259  rebtwn2z  9263  modqid  9351  modqcyc  9361  mulqaddmodid  9366  modqadd2mod  9376  addmodlteq  9400  facndiv  9666  faclbnd  9668  ibcval5  9690  caucvgre  9867  resqrexlemlo  9899  cau3lem  10000  qdenre  10088  rexico  10107  fimaxre2  10109  2clim  10140  cn1lem  10152  climsqz  10173  climsqz2  10174  climcau  10184  zdvdsdc  10216  dvdseq  10248  dvdsext  10255  odd2np1  10272  sqoddm1div8z  10286  nno  10306  zsupcllemstep  10341  infssuzex  10345  dfgcd3  10399  dvdslcm  10451  lcmneg  10456  lcmgcdlem  10459  ncoprmgcdne1b  10471  qredeq  10478  qredeu  10479  divgcdcoprm0  10483  exprmfct  10519  prmdvdsfz  10520  rpexp1i  10533  sqrt2irr  10541