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  1161  3adant1l  1230  reu6  2928  sbc2iegf  3035  sbcralt  3041  sbcrext  3042  indifdir  3393  pofun  4314  poinxp  4697  ssimaex  5579  fndmdif  5623  dffo4  5666  fcompt  5688  fconst2g  5733  foco2  5756  foeqcnvco  5793  f1eqcocnv  5794  fliftel1  5797  isores3  5818  acexmid  5876  tfrlemi14d  6336  tfrcl  6367  dom2lem  6774  fiintim  6930  ordiso2  7036  mkvprop  7158  lt2addnq  7405  lt2mulnq  7406  ltexnqq  7409  genpdf  7509  addnqprl  7530  addnqpru  7531  addlocpr  7537  recexprlemopl  7626  caucvgsrlemgt1  7796  add4  8120  cnegex  8137  ltleadd  8405  zextle  9346  peano5uzti  9363  fnn0ind  9371  xrlttr  9797  xaddass  9871  iccshftr  9996  iccshftl  9998  iccdil  10000  icccntr  10002  fzaddel  10061  fzrev  10086  exbtwnzlemshrink  10251  seq3val  10460  iseqf1olemab  10491  exp3vallem  10523  mulexp  10561  expadd  10564  expmul  10567  leexp1a  10577  bccl  10749  hashfacen  10818  ovshftex  10830  2shfti  10842  caucvgre  10992  cvg1nlemcau  10995  resqrexlemcvg  11030  cau3lem  11125  rexico  11232  iooinsup  11287  climmpt  11310  subcn2  11321  climrecvg1n  11358  climcvg1nlem  11359  climcaucn  11361  mertenslem2  11546  eftlcl  11698  reeftlcl  11699  dvdsext  11863  sqoddm1div8z  11893  bezoutlemaz  12006  bezoutr1  12036  dvdslcm  12071  lcmeq0  12073  lcmcl  12074  lcmneg  12076  lcmdvds  12081  coprmgcdb  12090  dvdsprime  12124  pc2dvds  12331  prmpwdvds  12355  infpnlem1  12359  1arith  12367  mhmco  12879  mhmima  12880  dfgrp2  12907  mulgfng  12992  subgintm  13063  islmod  13386  islmodd  13388  cnco  13760  cnss1  13765  tx2cn  13809  upxp  13811  metss  14033  txmetcnp  14057  cncfss  14109  cosz12  14240  bj-findis  14770