Theorem adantll 468

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  ad2antlr  481  ad2ant2l  500  ad2ant2lr  502  ad5ant23  514  ad5ant24  515  ad5ant25  516  3ad2antl3  1150  3adant1l  1219  reu6  2910  sbc2iegf  3016  sbcralt  3022  sbcrext  3023  indifdir  3373  pofun  4284  poinxp  4667  ssimaex  5541  fndmdif  5584  dffo4  5627  fcompt  5649  fconst2g  5694  foco2  5716  foeqcnvco  5752  f1eqcocnv  5753  fliftel1  5756  isores3  5777  acexmid  5835  tfrlemi14d  6292  tfrcl  6323  dom2lem  6729  fiintim  6885  ordiso2  6991  mkvprop  7113  lt2addnq  7336  lt2mulnq  7337  ltexnqq  7340  genpdf  7440  addnqprl  7461  addnqpru  7462  addlocpr  7468  recexprlemopl  7557  caucvgsrlemgt1  7727  add4  8050  cnegex  8067  ltleadd  8335  zextle  9273  peano5uzti  9290  fnn0ind  9298  xrlttr  9722  xaddass  9796  iccshftr  9921  iccshftl  9923  iccdil  9925  icccntr  9927  fzaddel  9984  fzrev  10009  exbtwnzlemshrink  10174  seq3val  10383  iseqf1olemab  10414  exp3vallem  10446  mulexp  10484  expadd  10487  expmul  10490  leexp1a  10500  bccl  10669  hashfacen  10735  ovshftex  10747  2shfti  10759  caucvgre  10909  cvg1nlemcau  10912  resqrexlemcvg  10947  cau3lem  11042  rexico  11149  iooinsup  11204  climmpt  11227  subcn2  11238  climrecvg1n  11275  climcvg1nlem  11276  climcaucn  11278  mertenslem2  11463  eftlcl  11615  reeftlcl  11616  dvdsext  11778  sqoddm1div8z  11808  bezoutlemaz  11921  bezoutr1  11951  dvdslcm  11980  lcmeq0  11982  lcmcl  11983  lcmneg  11985  lcmdvds  11990  coprmgcdb  11999  dvdsprime  12033  pc2dvds  12238  cnco  12762  cnss1  12767  tx2cn  12811  upxp  12813  metss  13035  txmetcnp  13059  cncfss  13111  cosz12  13242  bj-findis  13696