Theorem adantll 463

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 109	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜑)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan 279	1 ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  ad2antlr  476  ad2ant2l  495  ad2ant2lr  497  3ad2antl3  1113  3adant1l  1176  reu6  2826  sbc2iegf  2931  sbcralt  2937  sbcrext  2938  indifdir  3279  pofun  4172  poinxp  4546  ssimaex  5414  fndmdif  5457  dffo4  5500  fcompt  5522  fconst2g  5567  foco2  5587  foeqcnvco  5623  f1eqcocnv  5624  fliftel1  5627  isores3  5648  acexmid  5705  tfrlemi14d  6160  tfrcl  6191  dom2lem  6596  fiintim  6746  ordiso2  6835  mkvprop  6943  lt2addnq  7113  lt2mulnq  7114  ltexnqq  7117  genpdf  7217  addnqprl  7238  addnqpru  7239  addlocpr  7245  recexprlemopl  7334  caucvgsrlemgt1  7490  add4  7794  cnegex  7811  ltleadd  8075  zextle  8994  peano5uzti  9011  fnn0ind  9019  xrlttr  9422  xaddass  9493  iccshftr  9618  iccshftl  9620  iccdil  9622  icccntr  9624  fzaddel  9680  fzrev  9705  exbtwnzlemshrink  9867  seq3val  10072  iseqf1olemab  10103  exp3vallem  10135  mulexp  10173  expadd  10176  expmul  10179  leexp1a  10189  bccl  10354  hashfacen  10420  ovshftex  10432  2shfti  10444  caucvgre  10593  cvg1nlemcau  10596  resqrexlemcvg  10631  cau3lem  10726  rexico  10833  iooinsup  10885  climmpt  10908  subcn2  10919  climrecvg1n  10956  climcvg1nlem  10957  climcaucn  10959  mertenslem2  11144  eftlcl  11192  reeftlcl  11193  dvdsext  11348  sqoddm1div8z  11378  bezoutlemaz  11484  bezoutr1  11514  dvdslcm  11543  lcmeq0  11545  lcmcl  11546  lcmneg  11548  lcmdvds  11553  coprmgcdb  11562  dvdsprime  11596  cnco  12171  cnss1  12176  tx2cn  12220  upxp  12222  metss  12422  cncfss  12483  bj-findis  12762