Theorem ad2antlr 473

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 460	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  477  simplr  497  simplrl  502  simplrr  503  ordtri2or2exmidlem  4308  en2lp  4336  xpid11m  4619  foun  5223  f1oprg  5246  fcof1o  5511  foeqcnvco  5512  f1eqcocnv  5513  caovord3  5756  f1o2ndf1  5931  smores2  5994  frecrdg  6108  nnaordex  6219  xpdom2  6480  xpen  6494  mapen  6495  xpmapenlem  6498  nndomo  6513  phpm  6514  fidifsnen  6519  isinfinf  6546  finexdc  6548  fientri3  6555  xpfi  6568  f1dmvrnfibi  6581  sbthlemi8  6594  djudom  6708  enomnilem  6715  finomni  6717  exmidfodomrlemrALT  6750  dfplpq2  6834  recclnq  6872  subhalfnqq  6894  distrnq0  6939  prarloclem3step  6976  genpml  6997  genpmu  6998  addnqprl  7009  addnqpru  7010  appdivnq  7043  mulnqprl  7048  mulnqpru  7049  mullocpr  7051  ltexprlemfl  7089  ltexprlemfu  7091  ltmprr  7122  archpr  7123  cauappcvgprlemm  7125  caucvgprlemladdrl  7158  caucvgprprlemopl  7177  caucvgprprlemopu  7179  recexgt0sr  7240  mulgt0sr  7244  elrealeu  7288  axcaucvglemcau  7354  axcaucvglemres  7355  cnegex  7581  apirr  8000  mulge0  8014  lemul12a  8235  lediv2a  8268  creur  8331  nndiv  8374  zaddcllemneg  8699  peano5uzti  8764  supinfneg  8992  infsupneg  8993  divfnzn  9015  xrltso  9175  elioc2  9263  elico2  9264  elicc2  9265  exfzdc  9554  exbtwnzlemex  9564  rebtwn2z  9569  modqid  9659  modqcyc  9669  mulqaddmodid  9674  modqadd2mod  9684  addmodlteq  9708  frecuzrdgg  9726  iseqvalt  9765  iseqoveq  9773  facndiv  9996  faclbnd  9998  ibcval5  10020  hashen  10041  fihashdom  10060  hashunlem  10061  hashfacen  10089  caucvgre  10255  resqrexlemlo  10287  cau3lem  10388  qdenre  10476  rexico  10495  fimaxre2  10497  2clim  10528  cn1lem  10540  climsqz  10561  climsqz2  10562  climcau  10572  isumrblem  10587  zdvdsdc  10611  dvdseq  10643  dvdsext  10650  odd2np1  10667  sqoddm1div8z  10680  nno  10700  zsupcllemstep  10735  infssuzex  10739  dfgcd3  10793  dvdslcm  10845  lcmneg  10850  lcmgcdlem  10853  ncoprmgcdne1b  10865  qredeq  10872  qredeu  10873  divgcdcoprm0  10877  exprmfct  10913  prmdvdsfz  10914  rpexp1i  10927  sqrt2irr  10935  nonsq  10979  nnsf  11251  peano4nninf  11252  nninfalllemn  11254  nninfalllem1  11255  nninfsellemqall  11263  nninfsellemeqinf  11264  exmidsbthrlem  11268