Theorem adantlr 468

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
adantlr	⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)

Proof of Theorem adantlr

Step	Hyp	Ref	Expression
1		simpl 108	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜑)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan 281	1 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad2antrr  479  ad2ant2r  500  ad2ant2rl  502  adantl3r  503  ad4ant14  505  ad4ant24  507  ad5ant13  510  ad5ant14  511  ad5ant15  512  3ad2antl1  1143  3ad2antl2  1144  ad4ant124  1194  3adant1r  1209  bilukdc  1374  intab  3795  pofun  4229  ralxfrd  4378  rexxfrd  4379  ordtri2or2exmidlem  4436  wessep  4487  poinxp  4603  relop  4684  fun11iun  5381  ssimaex  5475  fndmdif  5518  fconst2g  5628  foeqcnvco  5684  f1eqcocnv  5685  isocnv  5705  isocnv2  5706  riota2df  5743  grprinvd  5959  grpridd  5960  f1o2ndf1  6118  tfr1onlembacc  6232  tfr1onlemaccex  6238  tfr1onlemres  6239  tfrcllembacc  6245  tfrcllemaccex  6251  tfrcllemres  6252  tfrcldm  6253  tfrcl  6254  xpdom2  6718  fimax2gtrilemstep  6787  xpfi  6811  eqsupti  6876  ordiso2  6913  enumctlemm  6992  mulcanpig  7136  prarloclemlt  7294  genpdf  7309  genpdisj  7324  addnqprl  7330  addnqpru  7331  addlocpr  7337  prmuloc  7367  mulnqprl  7369  mulnqpru  7370  mullocpr  7372  ltpopr  7396  ltsopr  7397  ltaddpr  7398  ltexprlemdisj  7407  ltexprlemloc  7408  ltexprlemru  7413  addcanprleml  7415  addcanprlemu  7416  ltaprg  7420  recexprlemopu  7428  recexprlemloc  7432  cauappcvgprlemladdfl  7456  cauappcvgprlemladdru  7457  caucvgsrlemcau  7594  caucvgsrlemgt1  7596  caucvgsrlemoffcau  7599  caucvgsrlemoffres  7601  suplocsrlem  7609  axcaucvglemcau  7699  axpre-suploclemres  7702  axsuploc  7830  cnegexlem1  7930  cnegexlem3  7932  cnegex  7933  addsubeq4  7970  rimul  8340  divcanap6  8472  ltmul12a  8611  lemul12b  8612  lbinf  8699  zrevaddcl  9097  nzadd  9099  zextle  9135  fzind  9159  uz11  9341  qreccl  9427  qrevaddcl  9429  irradd  9431  xrlttr  9574  xrltso  9575  xaddass  9645  xleadd1a  9649  xlt2add  9656  iccshftr  9770  iccshftl  9772  iccdil  9774  icccntr  9776  divelunit  9778  uzsubsubfz  9820  fzaddel  9832  fzrev  9857  elfzmlbp  9902  frec2uzrdg  10175  frecuzrdgtcl  10178  frecuzrdgsuc  10180  frecuzrdgdomlem  10183  frecuzrdgfunlem  10185  frecuzrdgsuctlem  10189  iseqovex  10222  seq3val  10224  seqf  10227  seq3clss  10233  seq3fveq2  10235  seq3feq2  10236  seq3feq  10238  seq3shft2  10239  ser3mono  10244  seq3split  10245  seq3caopr3  10247  seq3caopr2  10248  iseqf1olemab  10255  seq3f1olemqsumkj  10264  seq3f1olemqsumk  10265  seq3f1olemqsum  10266  seq3f1olemstep  10267  seq3f1oleml  10269  seq3id3  10273  seq3id  10274  seq3id2  10275  seq3homo  10276  seq3z  10277  seqfeq3  10278  ser3ge0  10283  expp1  10293  expnegap0  10294  expcllem  10297  mulexp  10325  expadd  10328  expaddzap  10330  expmulzap  10332  expdivap  10337  leexp1a  10341  expnlbnd  10409  bcpasc  10505  bccl  10506  hashfacen  10572  seq3coll  10578  seq3shft  10603  resqrexlemfp1  10774  sqrtdiv  10807  climshftlemg  11064  climcn1  11070  climsqz  11097  climsqz2  11098  clim2ser  11099  clim2ser2  11100  isermulc2  11102  climub  11106  serf0  11114  fsum3cvg  11139  sumrbdc  11140  summodclem3  11142  summodclem2a  11143  zsumdc  11146  fsumf1o  11152  isumss  11153  fisumss  11154  isumss2  11155  fsum3cvg2  11156  fsum3cvg3  11158  fsumcl2lem  11160  fsumcllem  11161  fsumadd  11168  fsumsplit  11169  fsumsplitsn  11172  sumsplitdc  11194  fisumrev2  11208  fsum2mul  11215  fsum00  11224  telfsumo  11228  fsumparts  11232  iserabs  11237  cvgratnnlemabsle  11289  cvgratnn  11293  cvgratz  11294  mertenslemub  11296  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  clim2prod  11301  clim2divap  11302  prodfap0  11307  prodfrecap  11308  prodeq2  11319  fproddccvg  11334  prodrbdclem2  11335  eftlcvg  11382  negdvdsb  11498  dvdsnegb  11499  dvdsext  11542  addmodlteqALT  11546  nno  11592  infssuzex  11631  gcdsupex  11635  gcdsupcl  11636  bezoutlembz  11681  dvdssq  11708  eucalgf  11725  dvdslcm  11739  lcmledvds  11740  lcmeq0  11741  lcmcl  11742  lcmdvds  11749  lcmgcdeq  11753  divgcdcoprmex  11772  phibndlem  11881  phiprmpw  11887  ctiunctlemf  11940  ctiunct  11942  opnssneib  12314  neissex  12323  tgrest  12327  iscnp3  12361  cnpnei  12377  cnrest  12393  tx1cn  12427  txcnp  12429  elbl3ps  12552  elbl3  12553  blininf  12582  blssexps  12587  blssex  12588  blpnfctr  12597  mopni2  12641  blsscls2  12651  metss  12652  bdmet  12660  metrest  12664  metcn  12672  txmetcn  12677  bl2ioo  12700  ivthinclemlr  12773  ivthinclemur  12775  dvcj  12831  dvfre  12832  coseq0q4123  12904  abssinper  12916  subctctexmid  13185  cvgcmp2n  13217