Theorem adantll 476

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 ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  ad2antlr  489  ad2ant2l  508  ad2ant2lr  510  ad5ant23  522  ad5ant24  523  ad5ant25  524  3ad2antl3  1185  3adant1l  1254  reu6  2992  sbc2iegf  3099  sbcralt  3105  sbcrext  3106  indifdir  3460  pofun  4403  poinxp  4788  ssimaex  5697  fndmdif  5742  dffo4  5785  fcompt  5807  fconst2g  5858  foco2  5883  foeqcnvco  5920  f1eqcocnv  5921  fliftel1  5924  isores3  5945  acexmid  6006  tfrlemi14d  6485  tfrcl  6516  dom2lem  6931  fiintim  7104  ordiso2  7213  mkvprop  7336  lt2addnq  7602  lt2mulnq  7603  ltexnqq  7606  genpdf  7706  addnqprl  7727  addnqpru  7728  addlocpr  7734  recexprlemopl  7823  caucvgsrlemgt1  7993  add4  8318  cnegex  8335  ltleadd  8604  zextle  9549  peano5uzti  9566  fnn0ind  9574  xrlttr  10003  xaddass  10077  iccshftr  10202  iccshftl  10204  iccdil  10206  icccntr  10208  fzaddel  10267  fzrev  10292  exbtwnzlemshrink  10480  xqltnle  10499  seq3val  10694  iseqf1olemab  10736  seqf1og  10755  exp3vallem  10774  mulexp  10812  expadd  10815  expmul  10818  leexp1a  10828  bccl  11001  hashfacen  11071  wrdnval  11115  swrdccat3blem  11286  ovshftex  11345  2shfti  11357  caucvgre  11507  cvg1nlemcau  11510  resqrexlemcvg  11545  cau3lem  11640  rexico  11747  iooinsup  11803  climmpt  11826  subcn2  11837  climrecvg1n  11874  climcvg1nlem  11875  climcaucn  11877  mertenslem2  12062  eftlcl  12214  reeftlcl  12215  dvdsext  12381  3dvds  12390  sqoddm1div8z  12412  bezoutlemaz  12539  bezoutr1  12569  dvdslcm  12606  lcmeq0  12608  lcmcl  12609  lcmneg  12611  lcmdvds  12616  coprmgcdb  12625  dvdsprime  12659  pc2dvds  12868  prmpwdvds  12893  infpnlem1  12897  1arith  12905  resmhm  13535  resmhm2b  13537  mhmco  13538  mhmima  13539  gsumwsubmcl  13544  dfgrp2  13575  mulgfng  13676  subgintm  13750  ghmmhmb  13806  resghm  13812  islmod  14270  islmodd  14272  cnco  14910  cnss1  14915  tx2cn  14959  upxp  14961  metss  15183  txmetcnp  15207  cncfss  15272  plyaddlem1  15436  plymullem1  15437  cosz12  15469  gausslemma2dlem4  15758  bj-findis  16397