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  2949  sbc2iegf  3056  sbcralt  3062  sbcrext  3063  indifdir  3415  pofun  4343  poinxp  4728  ssimaex  5618  fndmdif  5663  dffo4  5706  fcompt  5728  fconst2g  5773  foco2  5796  foeqcnvco  5833  f1eqcocnv  5834  fliftel1  5837  isores3  5858  acexmid  5917  tfrlemi14d  6386  tfrcl  6417  dom2lem  6826  fiintim  6985  ordiso2  7094  mkvprop  7217  lt2addnq  7464  lt2mulnq  7465  ltexnqq  7468  genpdf  7568  addnqprl  7589  addnqpru  7590  addlocpr  7596  recexprlemopl  7685  caucvgsrlemgt1  7855  add4  8180  cnegex  8197  ltleadd  8465  zextle  9408  peano5uzti  9425  fnn0ind  9433  xrlttr  9861  xaddass  9935  iccshftr  10060  iccshftl  10062  iccdil  10064  icccntr  10066  fzaddel  10125  fzrev  10150  exbtwnzlemshrink  10317  xqltnle  10336  seq3val  10531  iseqf1olemab  10573  seqf1og  10592  exp3vallem  10611  mulexp  10649  expadd  10652  expmul  10655  leexp1a  10665  bccl  10838  hashfacen  10907  wrdnval  10944  ovshftex  10963  2shfti  10975  caucvgre  11125  cvg1nlemcau  11128  resqrexlemcvg  11163  cau3lem  11258  rexico  11365  iooinsup  11420  climmpt  11443  subcn2  11454  climrecvg1n  11491  climcvg1nlem  11492  climcaucn  11494  mertenslem2  11679  eftlcl  11831  reeftlcl  11832  dvdsext  11997  sqoddm1div8z  12027  bezoutlemaz  12140  bezoutr1  12170  dvdslcm  12207  lcmeq0  12209  lcmcl  12210  lcmneg  12212  lcmdvds  12217  coprmgcdb  12226  dvdsprime  12260  pc2dvds  12468  prmpwdvds  12493  infpnlem1  12497  1arith  12505  resmhm  13059  resmhm2b  13061  mhmco  13062  mhmima  13063  gsumwsubmcl  13068  dfgrp2  13099  mulgfng  13194  subgintm  13268  ghmmhmb  13324  resghm  13330  islmod  13787  islmodd  13789  cnco  14389  cnss1  14394  tx2cn  14438  upxp  14440  metss  14662  txmetcnp  14686  cncfss  14738  plyaddlem1  14893  plymullem1  14894  cosz12  14915  gausslemma2dlem4  15180  bj-findis  15471