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  1187  3adant1l  1256  reu6  2995  sbc2iegf  3102  sbcralt  3108  sbcrext  3109  indifdir  3463  pofun  4409  poinxp  4795  ssimaex  5707  fndmdif  5752  dffo4  5795  fcompt  5817  fconst2g  5868  foco2  5893  foeqcnvco  5930  f1eqcocnv  5931  fliftel1  5934  isores3  5955  acexmid  6016  tfrlemi14d  6498  tfrcl  6529  dom2lem  6944  fiintim  7122  ordiso2  7233  mkvprop  7356  lt2addnq  7623  lt2mulnq  7624  ltexnqq  7627  genpdf  7727  addnqprl  7748  addnqpru  7749  addlocpr  7755  recexprlemopl  7844  caucvgsrlemgt1  8014  add4  8339  cnegex  8356  ltleadd  8625  zextle  9570  peano5uzti  9587  fnn0ind  9595  xrlttr  10029  xaddass  10103  iccshftr  10228  iccshftl  10230  iccdil  10232  icccntr  10234  fzaddel  10293  fzrev  10318  exbtwnzlemshrink  10507  xqltnle  10526  seq3val  10721  iseqf1olemab  10763  seqf1og  10782  exp3vallem  10801  mulexp  10839  expadd  10842  expmul  10845  leexp1a  10855  bccl  11028  hashfacen  11099  wrdnval  11143  swrdccat3blem  11319  ovshftex  11379  2shfti  11391  caucvgre  11541  cvg1nlemcau  11544  resqrexlemcvg  11579  cau3lem  11674  rexico  11781  iooinsup  11837  climmpt  11860  subcn2  11871  climrecvg1n  11908  climcvg1nlem  11909  climcaucn  11911  mertenslem2  12096  eftlcl  12248  reeftlcl  12249  dvdsext  12415  3dvds  12424  sqoddm1div8z  12446  bezoutlemaz  12573  bezoutr1  12603  dvdslcm  12640  lcmeq0  12642  lcmcl  12643  lcmneg  12645  lcmdvds  12650  coprmgcdb  12659  dvdsprime  12693  pc2dvds  12902  prmpwdvds  12927  infpnlem1  12931  1arith  12939  resmhm  13569  resmhm2b  13571  mhmco  13572  mhmima  13573  gsumwsubmcl  13578  dfgrp2  13609  mulgfng  13710  subgintm  13784  ghmmhmb  13840  resghm  13846  islmod  14304  islmodd  14306  cnco  14944  cnss1  14949  tx2cn  14993  upxp  14995  metss  15217  txmetcnp  15241  cncfss  15306  plyaddlem1  15470  plymullem1  15471  cosz12  15503  gausslemma2dlem4  15792  egrsubgr  16113  bj-findis  16574