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  1163  3adant1l  1232  reu6  2941  sbc2iegf  3048  sbcralt  3054  sbcrext  3055  indifdir  3406  pofun  4330  poinxp  4713  ssimaex  5598  fndmdif  5642  dffo4  5685  fcompt  5707  fconst2g  5752  foco2  5775  foeqcnvco  5812  f1eqcocnv  5813  fliftel1  5816  isores3  5837  acexmid  5896  tfrlemi14d  6359  tfrcl  6390  dom2lem  6799  fiintim  6958  ordiso2  7065  mkvprop  7187  lt2addnq  7434  lt2mulnq  7435  ltexnqq  7438  genpdf  7538  addnqprl  7559  addnqpru  7560  addlocpr  7566  recexprlemopl  7655  caucvgsrlemgt1  7825  add4  8149  cnegex  8166  ltleadd  8434  zextle  9375  peano5uzti  9392  fnn0ind  9400  xrlttr  9827  xaddass  9901  iccshftr  10026  iccshftl  10028  iccdil  10030  icccntr  10032  fzaddel  10091  fzrev  10116  exbtwnzlemshrink  10281  xqltnle  10300  seq3val  10491  iseqf1olemab  10522  exp3vallem  10555  mulexp  10593  expadd  10596  expmul  10599  leexp1a  10609  bccl  10782  hashfacen  10851  ovshftex  10863  2shfti  10875  caucvgre  11025  cvg1nlemcau  11028  resqrexlemcvg  11063  cau3lem  11158  rexico  11265  iooinsup  11320  climmpt  11343  subcn2  11354  climrecvg1n  11391  climcvg1nlem  11392  climcaucn  11394  mertenslem2  11579  eftlcl  11731  reeftlcl  11732  dvdsext  11896  sqoddm1div8z  11926  bezoutlemaz  12039  bezoutr1  12069  dvdslcm  12104  lcmeq0  12106  lcmcl  12107  lcmneg  12109  lcmdvds  12114  coprmgcdb  12123  dvdsprime  12157  pc2dvds  12365  prmpwdvds  12390  infpnlem1  12394  1arith  12402  resmhm  12954  resmhm2b  12956  mhmco  12957  mhmima  12958  dfgrp2  12986  mulgfng  13081  subgintm  13154  ghmmhmb  13210  resghm  13216  islmod  13624  islmodd  13626  cnco  14198  cnss1  14203  tx2cn  14247  upxp  14249  metss  14471  txmetcnp  14495  cncfss  14547  cosz12  14678  bj-findis  15209