Theorem adantlr 477

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 109	. 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:  ad2antrr  488  ad2ant2r  509  ad2ant2rl  511  adantl3r  512  ad4ant14  514  ad4ant24  516  ad5ant13  519  ad5ant14  520  ad5ant15  521  3ad2antl1  1186  3ad2antl2  1187  ad4ant124  1243  3adant1r  1258  ad5ant235  1265  ad5ant135  1270  bilukdc  1441  ifeqeqxdc  3673  elpr2elpr  3885  intab  3983  pofun  4438  ralxfrd  4588  rexxfrd  4589  ordtri2or2exmidlem  4653  wessep  4705  poinxp  4824  relop  4910  fun11iun  5640  ssimaex  5743  fndmdif  5788  fconst2g  5904  foeqcnvco  5969  f1eqcocnv  5970  isocnv  5990  isocnv2  5991  riota2df  6033  caofdig  6309  f1o2ndf1  6437  tfr1onlembacc  6586  tfr1onlemaccex  6592  tfr1onlemres  6593  tfrcllembacc  6599  tfrcllemaccex  6605  tfrcllemres  6606  tfrcldm  6607  tfrcl  6608  xpdom2  7095  fimax2gtrilemstep  7171  xpfi  7205  eqsupti  7300  ordiso2  7339  enumctlemm  7418  enwomnilem  7473  cc2lem  7596  mulcanpig  7666  prarloclemlt  7824  genpdf  7839  genpdisj  7854  addnqprl  7860  addnqpru  7861  addlocpr  7867  prmuloc  7897  mulnqprl  7899  mulnqpru  7900  mullocpr  7902  ltpopr  7926  ltsopr  7927  ltaddpr  7928  ltexprlemdisj  7937  ltexprlemloc  7938  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  ltaprg  7950  recexprlemopu  7958  recexprlemloc  7962  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  caucvgsrlemcau  8124  caucvgsrlemgt1  8126  caucvgsrlemoffcau  8129  caucvgsrlemoffres  8131  suplocsrlem  8139  axcaucvglemcau  8229  axpre-suploclemres  8232  axsuploc  8362  cnegexlem1  8465  cnegexlem3  8467  cnegex  8468  addsubeq4  8505  rimul  8877  divcanap6  9013  ltmul12a  9154  lemul12b  9155  lbinf  9242  zrevaddcl  9648  nzadd  9650  zextle  9690  fzind  9714  uz11  9898  infregelbex  9951  qreccl  9995  qrevaddcl  9997  irradd  9999  xrlttr  10150  xrltso  10151  xaddass  10224  xleadd1a  10228  xlt2add  10235  iccshftr  10349  iccshftl  10351  iccdil  10353  icccntr  10355  divelunit  10357  uzsubsubfz  10404  fzaddel  10417  fzrev  10443  elfzmlbp  10491  infssuzex  10618  zsupssdc  10625  frec2uzrdg  10798  frecuzrdgtcl  10801  frecuzrdgsuc  10803  frecuzrdgdomlem  10806  frecuzrdgfunlem  10808  frecuzrdgsuctlem  10812  iseqovex  10847  seq3val  10849  seqf  10853  seq3clss  10860  seq3fveq2  10864  seq3feq2  10865  seq3feq  10869  seq3shft2  10870  ser3mono  10876  seq3split  10877  seqsplitg  10878  seq3caopr3  10880  seq3caopr2  10882  seqcaopr2g  10883  iseqf1olemab  10891  seq3f1olemqsumkj  10900  seq3f1olemqsumk  10901  seq3f1olemqsum  10902  seq3f1olemstep  10903  seq3f1oleml  10905  seqf1oglem2a  10907  seqf1oglem2  10909  seq3id3  10913  seq3id  10914  seq3id2  10915  seq3homo  10916  seq3z  10917  seqfeq3  10918  seqhomog  10919  seqfeq4g  10920  ser3ge0  10925  expp1  10935  expnegap0  10936  expcllem  10939  mulexp  10967  expadd  10970  expaddzap  10972  expmulzap  10974  expdivap  10979  leexp1a  10983  expnlbnd  11054  bcpasc  11156  bccl  11157  hashfacen  11236  seq3coll  11242  ccatlen  11311  ccatvalfn  11317  ccatsymb  11318  ccatalpha  11329  pfxclz  11399  wrd2ind  11443  swrdccat  11455  seq3shft  11551  resqrexlemfp1  11722  sqrtdiv  11755  climshftlemg  12015  climcn1  12021  climsqz  12048  climsqz2  12049  clim2ser  12050  clim2ser2  12051  isermulc2  12053  climub  12057  serf0  12065  fsum3cvg  12092  sumrbdc  12093  summodclem3  12094  summodclem2a  12095  zsumdc  12098  fsumf1o  12104  isumss  12105  fisumss  12106  isumss2  12107  fsum3cvg2  12108  fsum3cvg3  12110  fsumcl2lem  12112  fsumcllem  12113  fsumadd  12120  fsumsplit  12121  fsumsplitsn  12124  sumsplitdc  12146  fisumrev2  12160  fsum2mul  12167  fsum00  12176  telfsumo  12180  fsumparts  12184  iserabs  12189  cvgratnnlemabsle  12241  cvgratnn  12245  cvgratz  12246  mertenslemub  12248  mertenslemi1  12249  mertenslem2  12250  mertensabs  12251  clim2prod  12253  clim2divap  12254  prodfap0  12259  prodfrecap  12260  prodeq2  12271  fproddccvg  12286  prodrbdclem2  12287  prodmodc  12292  zproddc  12293  fprodf1o  12302  fprodssdc  12304  fprodunsn  12318  fprodcllem  12320  fprodabs  12330  fprodeq0  12331  fprodmodd  12355  eftlcvg  12401  negdvdsb  12521  dvdsnegb  12522  fsumdvds  12556  dvdsext  12569  addmodlteqALT  12573  nno  12620  gcdsupex  12681  gcdsupcl  12682  bezoutlembz  12728  dvdssq  12755  eucalgf  12780  dvdslcm  12794  lcmledvds  12795  lcmeq0  12796  lcmcl  12797  lcmdvds  12804  lcmgcdeq  12808  divgcdcoprmex  12827  isprm5lem  12866  phibndlem  12941  phiprmpw  12947  pc2dvds  13056  pcmpt  13069  prmpwdvds  13081  1arith  13093  4sqleminfi  13123  ballotfilemic  13197  ballotfilem1c  13198  ballotfilemsv  13200  ballotfilemsima  13206  ctiunctlemf  13276  ctiunct  13278  grpinva  13652  grprida  13653  gsumpropd2  13659  sgrppropd  13679  mndpropd  13704  mhmpropd  13724  0mhm  13744  resmhm2  13746  resmhm2b  13747  grplcan  13820  mulgval  13878  mulgnn0z  13905  mulgnndir  13907  mulgnn0dir  13908  issubg2m  13945  issubg4m  13949  subgintm  13954  ghmf1  14029  gsumfzmptfidmadd  14095  gsumfzmhm  14099  prdssgrpd  14136  prdsidlem  14138  prdsmndd  14139  srglmhm  14239  srgrmhm  14240  ringpropd  14284  crngpropd  14285  ringlghm  14307  ringrghm  14308  mulgass3  14332  issubrng2  14459  subrngpropd  14465  issubrg2  14490  subrgintm  14492  subrgpropd  14502  rhmpropd  14503  unitrrg  14517  lmodprop2d  14625  islss3  14656  lssintclm  14661  qusrhm  14805  gsumfzfsum  14865  opnssneib  15150  neissex  15159  tgrest  15163  iscnp3  15197  cnpnei  15213  cnrest  15229  tx1cn  15263  txcnp  15265  elbl3ps  15388  elbl3  15389  blininf  15418  blssexps  15423  blssex  15424  blpnfctr  15433  mopni2  15477  blsscls2  15487  metss  15488  bdmet  15496  metrest  15500  metcn  15508  txmetcn  15513  bl2ioo  15544  ivthinclemlr  15631  ivthinclemur  15633  dvcj  15703  dvfre  15704  elplyd  15735  plyaddlem1  15741  plymullem1  15742  plymullem  15744  plycolemc  15752  plycjlemc  15754  coseq0q4123  15828  abssinper  15840  fsumdvdsmul  15988  lgsval2lem  16012  lgsval4lem  16013  lgsneg  16026  lgsmod  16028  lgsdir2  16035  lgsdir  16037  lgsne0  16040  lgssq  16042  lgsquadlem1  16079  usgredg2vlem2  16347  clwwlkccat  16525  clwwlknonex2lem2  16562  subctctexmid  16913  cvgcmp2n  16956  iswomninnlem  16973  nconstwlpo  16991