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  4314  en2lp  4342  xpid11m  4625  foun  5229  f1oprg  5252  fcof1o  5523  foeqcnvco  5524  f1eqcocnv  5525  caovord3  5769  f1o2ndf1  5944  smores2  6007  frecrdg  6121  nnaordex  6232  xpdom2  6493  xpen  6507  mapen  6508  xpmapenlem  6511  nndomo  6526  phpm  6527  fidifsnen  6532  isinfinf  6559  finexdc  6564  fientri3  6571  xpfi  6584  f1dmvrnfibi  6597  sbthlemi8  6610  djudom  6724  enomnilem  6731  finomni  6733  exmidfodomrlemrALT  6766  dfplpq2  6850  recclnq  6888  subhalfnqq  6910  distrnq0  6955  prarloclem3step  6992  genpml  7013  genpmu  7014  addnqprl  7025  addnqpru  7026  appdivnq  7059  mulnqprl  7064  mulnqpru  7065  mullocpr  7067  ltexprlemfl  7105  ltexprlemfu  7107  ltmprr  7138  archpr  7139  cauappcvgprlemm  7141  caucvgprlemladdrl  7174  caucvgprprlemopl  7193  caucvgprprlemopu  7195  recexgt0sr  7256  mulgt0sr  7260  elrealeu  7304  axcaucvglemcau  7370  axcaucvglemres  7371  cnegex  7597  apirr  8016  mulge0  8030  lemul12a  8251  lediv2a  8284  creur  8347  nndiv  8390  zaddcllemneg  8715  peano5uzti  8780  supinfneg  9008  infsupneg  9009  divfnzn  9031  xrltso  9191  elioc2  9279  elico2  9280  elicc2  9281  exfzdc  9572  exbtwnzlemex  9582  rebtwn2z  9587  modqid  9677  modqcyc  9687  mulqaddmodid  9692  modqadd2mod  9702  addmodlteq  9726  frecuzrdgg  9744  iseqvalt  9783  iseqoveq  9791  iseqf1olemqcl  9812  iseqf1olemnab  9814  iseqf1olemp  9828  iseqf1o  9830  fser0const  9842  facndiv  10036  faclbnd  10038  ibcval5  10060  hashen  10081  fihashdom  10100  hashunlem  10101  hashfacen  10130  zfz1isolemiso  10133  iseqcoll  10136  caucvgre  10302  resqrexlemlo  10334  cau3lem  10435  qdenre  10523  rexico  10542  fimaxre2  10544  2clim  10575  cn1lem  10587  climsqz  10608  climsqz2  10609  climcau  10619  isumrblem  10648  isummolem2a  10653  fisum  10658  zdvdsdc  10684  dvdseq  10716  dvdsext  10723  odd2np1  10740  sqoddm1div8z  10753  nno  10773  zsupcllemstep  10808  infssuzex  10812  dfgcd3  10866  dvdslcm  10918  lcmneg  10923  lcmgcdlem  10926  ncoprmgcdne1b  10938  qredeq  10945  qredeu  10946  divgcdcoprm0  10950  exprmfct  10986  prmdvdsfz  10987  rpexp1i  11000  sqrt2irr  11008  nonsq  11052  nnsf  11325  peano4nninf  11326  nninfalllemn  11328  nninfalllem1  11329  nninfsellemqall  11337  nninfsellemeqinf  11338  exmidsbthrlem  11342