Theorem adantll 480

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
adantll	⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)

Proof of Theorem adantll

Step	Hyp	Ref	Expression
1		simpr 110	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜑)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan 283	1 ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad2antlr  493  ad2ant2l  512  ad2ant2lr  514  ad5ant23  526  ad5ant24  527  ad5ant25  528  3ad2antl3  1192  3adant1l  1261  reu6  3015  sbc2iegf  3122  sbcralt  3128  sbcrext  3129  indifdir  3487  pofun  4457  poinxp  4844  ssimaex  5764  fndmdif  5814  dffo4  5856  fcompt  5878  fconst2g  5930  foco2  5959  foeqcnvco  5996  f1eqcocnv  5997  fliftel1  6000  isores3  6021  acexmid  6084  suppssdc  6500  tfrlemi14d  6604  tfrcl  6635  mapsnd  6970  dom2lem  7058  fiintim  7238  ordiso2  7376  mkvprop  7499  lt2addnq  7772  lt2mulnq  7773  ltexnqq  7776  genpdf  7876  addnqprl  7897  addnqpru  7898  addlocpr  7904  recexprlemopl  7993  caucvgsrlemgt1  8163  add4  8489  cnegex  8506  ltleadd  8776  zextle  9742  peano5uzti  9759  fnn0ind  9767  xrlttr  10208  xaddass  10282  iccshftr  10407  iccshftl  10409  iccdil  10411  icccntr  10413  fzaddel  10476  fzrev  10502  exbtwnzlemshrink  10694  xqltnle  10713  seq3val  10912  iseqf1olemab  10954  seqf1og  10973  exp3vallem  10992  mulexp  11030  expadd  11033  expmul  11036  leexp1a  11046  bccl  11221  hashfacen  11300  wrdnval  11351  swrdccat3blem  11527  ovshftex  11600  2shfti  11612  caucvgre  11763  cvg1nlemcau  11766  resqrexlemcvg  11801  cau3lem  11897  rexico  12004  iooinsup  12062  climmpt  12085  subcn2  12096  climrecvg1n  12133  climcvg1nlem  12134  climcaucn  12136  mertenslem2  12322  eftlcl  12474  reeftlcl  12475  dvdsext  12641  3dvds  12650  sqoddm1div8z  12672  bezoutlemaz  12799  bezoutr1  12829  dvdslcm  12866  lcmeq0  12868  lcmcl  12869  lcmneg  12871  lcmdvds  12876  coprmgcdb  12885  dvdsprime  12919  pc2dvds  13132  prmpwdvds  13157  infpnlem1  13161  1arith  13169  resmhm  13847  resmhm2b  13849  mhmco  13850  mhmima  13851  gzsumwsubmcl  13854  dfgrp2  13885  mulgfng  13980  subgintm  14054  ghmmhmb  14110  resghm  14116  cntzmhm  14167  islmod  14711  islmodd  14713  cnco  15413  cnss1  15418  tx2cn  15462  upxp  15464  metss  15686  txmetcnp  15710  cncfss  15775  plyaddlem1  15939  plymullem1  15940  cosz12  15973  bposlem3  16274  gausslemma2dlem4  16349  egrsubgr  16670  bj-findis  17171