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  2953  sbc2iegf  3060  sbcralt  3066  sbcrext  3067  indifdir  3420  pofun  4348  poinxp  4733  ssimaex  5625  fndmdif  5670  dffo4  5713  fcompt  5735  fconst2g  5780  foco2  5803  foeqcnvco  5840  f1eqcocnv  5841  fliftel1  5844  isores3  5865  acexmid  5924  tfrlemi14d  6400  tfrcl  6431  dom2lem  6840  fiintim  7001  ordiso2  7110  mkvprop  7233  lt2addnq  7490  lt2mulnq  7491  ltexnqq  7494  genpdf  7594  addnqprl  7615  addnqpru  7616  addlocpr  7622  recexprlemopl  7711  caucvgsrlemgt1  7881  add4  8206  cnegex  8223  ltleadd  8492  zextle  9436  peano5uzti  9453  fnn0ind  9461  xrlttr  9889  xaddass  9963  iccshftr  10088  iccshftl  10090  iccdil  10092  icccntr  10094  fzaddel  10153  fzrev  10178  exbtwnzlemshrink  10357  xqltnle  10376  seq3val  10571  iseqf1olemab  10613  seqf1og  10632  exp3vallem  10651  mulexp  10689  expadd  10692  expmul  10695  leexp1a  10705  bccl  10878  hashfacen  10947  wrdnval  10984  ovshftex  11003  2shfti  11015  caucvgre  11165  cvg1nlemcau  11168  resqrexlemcvg  11203  cau3lem  11298  rexico  11405  iooinsup  11461  climmpt  11484  subcn2  11495  climrecvg1n  11532  climcvg1nlem  11533  climcaucn  11535  mertenslem2  11720  eftlcl  11872  reeftlcl  11873  dvdsext  12039  3dvds  12048  sqoddm1div8z  12070  bezoutlemaz  12197  bezoutr1  12227  dvdslcm  12264  lcmeq0  12266  lcmcl  12267  lcmneg  12269  lcmdvds  12274  coprmgcdb  12283  dvdsprime  12317  pc2dvds  12526  prmpwdvds  12551  infpnlem1  12555  1arith  12563  resmhm  13191  resmhm2b  13193  mhmco  13194  mhmima  13195  gsumwsubmcl  13200  dfgrp2  13231  mulgfng  13332  subgintm  13406  ghmmhmb  13462  resghm  13468  islmod  13925  islmodd  13927  cnco  14565  cnss1  14570  tx2cn  14614  upxp  14616  metss  14838  txmetcnp  14862  cncfss  14927  plyaddlem1  15091  plymullem1  15092  cosz12  15124  gausslemma2dlem4  15413  bj-findis  15733