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  1185  3adant1l  1254  reu6  2992  sbc2iegf  3099  sbcralt  3105  sbcrext  3106  indifdir  3460  pofun  4402  poinxp  4787  ssimaex  5694  fndmdif  5739  dffo4  5782  fcompt  5804  fconst2g  5853  foco2  5876  foeqcnvco  5913  f1eqcocnv  5914  fliftel1  5917  isores3  5938  acexmid  5999  tfrlemi14d  6477  tfrcl  6508  dom2lem  6921  fiintim  7089  ordiso2  7198  mkvprop  7321  lt2addnq  7587  lt2mulnq  7588  ltexnqq  7591  genpdf  7691  addnqprl  7712  addnqpru  7713  addlocpr  7719  recexprlemopl  7808  caucvgsrlemgt1  7978  add4  8303  cnegex  8320  ltleadd  8589  zextle  9534  peano5uzti  9551  fnn0ind  9559  xrlttr  9987  xaddass  10061  iccshftr  10186  iccshftl  10188  iccdil  10190  icccntr  10192  fzaddel  10251  fzrev  10276  exbtwnzlemshrink  10463  xqltnle  10482  seq3val  10677  iseqf1olemab  10719  seqf1og  10738  exp3vallem  10757  mulexp  10795  expadd  10798  expmul  10801  leexp1a  10811  bccl  10984  hashfacen  11053  wrdnval  11097  swrdccat3blem  11266  ovshftex  11325  2shfti  11337  caucvgre  11487  cvg1nlemcau  11490  resqrexlemcvg  11525  cau3lem  11620  rexico  11727  iooinsup  11783  climmpt  11806  subcn2  11817  climrecvg1n  11854  climcvg1nlem  11855  climcaucn  11857  mertenslem2  12042  eftlcl  12194  reeftlcl  12195  dvdsext  12361  3dvds  12370  sqoddm1div8z  12392  bezoutlemaz  12519  bezoutr1  12549  dvdslcm  12586  lcmeq0  12588  lcmcl  12589  lcmneg  12591  lcmdvds  12596  coprmgcdb  12605  dvdsprime  12639  pc2dvds  12848  prmpwdvds  12873  infpnlem1  12877  1arith  12885  resmhm  13515  resmhm2b  13517  mhmco  13518  mhmima  13519  gsumwsubmcl  13524  dfgrp2  13555  mulgfng  13656  subgintm  13730  ghmmhmb  13786  resghm  13792  islmod  14249  islmodd  14251  cnco  14889  cnss1  14894  tx2cn  14938  upxp  14940  metss  15162  txmetcnp  15186  cncfss  15251  plyaddlem1  15415  plymullem1  15416  cosz12  15448  gausslemma2dlem4  15737  bj-findis  16300