Theorem adantlr 481

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad2antrr  492  ad2ant2r  513  ad2ant2rl  515  adantl3r  516  ad4ant14  518  ad4ant24  520  ad5ant13  523  ad5ant14  524  ad5ant15  525  3ad2antl1  1190  3ad2antl2  1191  ad4ant124  1247  3adant1r  1262  ad5ant235  1269  ad5ant135  1274  bilukdc  1445  ifeqeqxdc  3687  elpr2elpr  3901  intab  3999  pofun  4457  ralxfrd  4608  rexxfrd  4609  ordtri2or2exmidlem  4673  wessep  4725  poinxp  4844  relop  4930  fun11iun  5660  relndmfv  5728  ssimaex  5764  fndmdif  5814  fconst2g  5930  foeqcnvco  5996  f1eqcocnv  5997  isocnv  6017  isocnv2  6018  riota2df  6060  caofdig  6336  f1o2ndf1  6464  tfr1onlembacc  6613  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllembacc  6626  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  tfrcl  6635  xpdom2  7129  fimax2gtrilemstep  7205  xpfi  7239  eqsupti  7336  ordiso2  7375  enumctlemm  7454  enwomnilem  7509  cc2lem  7632  mulcanpig  7702  prarloclemlt  7860  genpdf  7875  genpdisj  7890  addnqprl  7896  addnqpru  7897  addlocpr  7903  prmuloc  7933  mulnqprl  7935  mulnqpru  7936  mullocpr  7938  ltpopr  7962  ltsopr  7963  ltaddpr  7964  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  ltaprg  7986  recexprlemopu  7994  recexprlemloc  7998  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  caucvgsrlemcau  8160  caucvgsrlemgt1  8162  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  suplocsrlem  8175  axcaucvglemcau  8265  axpre-suploclemres  8268  axsuploc  8398  cnegexlem1  8502  cnegexlem3  8504  cnegex  8505  addsubeq4  8542  rimul  8915  divcanap6  9051  ltmul12a  9192  lemul12b  9193  lbinf  9280  zrevaddcl  9699  nzadd  9701  zextle  9741  fzind  9765  uz11  9954  infregelbex  10007  qreccl  10051  qrevaddcl  10053  irradd  10055  xrlttr  10207  xrltso  10208  xaddass  10281  xleadd1a  10285  xlt2add  10292  iccshftr  10406  iccshftl  10408  iccdil  10410  icccntr  10412  divelunit  10414  uzsubsubfz  10462  fzaddel  10475  fzrev  10501  elfzmlbp  10549  infssuzex  10676  zsupssdc  10683  frec2uzrdg  10859  frecuzrdgtcl  10862  frecuzrdgsuc  10864  frecuzrdgdomlem  10867  frecuzrdgfunlem  10869  frecuzrdgsuctlem  10873  iseqovex  10908  seq3val  10910  seqf  10914  seq3clss  10921  seq3fveq2  10925  seq3feq2  10926  seq3feq  10930  seq3shft2  10931  ser3mono  10937  seq3split  10938  seqsplitg  10939  seq3caopr3  10941  seq3caopr2  10943  seqcaopr2g  10944  iseqf1olemab  10952  seq3f1olemqsumkj  10961  seq3f1olemqsumk  10962  seq3f1olemqsum  10963  seq3f1olemstep  10964  seq3f1oleml  10966  seqf1oglem2a  10968  seqf1oglem2  10970  seq3id3  10974  seq3id  10975  seq3id2  10976  seq3homo  10977  seq3z  10978  seqfeq3  10979  seqhomog  10980  seqfeq4g  10981  ser3ge0  10986  expp1  10996  expnegap0  10997  expcllem  11000  mulexp  11028  expadd  11031  expaddzap  11033  expmulzap  11035  expdivap  11040  leexp1a  11044  expnlbnd  11115  bcpasc  11218  bccl  11219  hashfacen  11298  seq3coll  11308  ccatlen  11377  ccatvalfn  11383  ccatsymb  11384  ccatalpha  11395  pfxclz  11465  wrd2ind  11509  swrdccat  11521  seq3shft  11617  resqrexlemfp1  11789  sqrtdiv  11822  climshftlemg  12084  climcn1  12090  climsqz  12117  climsqz2  12118  clim2ser  12119  clim2ser2  12120  isermulc2  12122  climub  12126  serf0  12134  fsum3cvg  12161  sumrbdc  12162  summodclem3  12163  summodclem2a  12164  zsumdc  12167  fsumf1o  12173  isumss  12174  fisumss  12175  isumss2  12176  fsum3cvg2  12177  fsum3cvg3  12179  fsumcl2lem  12181  fsumcllem  12182  fsumadd  12189  fsumsplit  12190  fsumsplitsn  12193  sumsplitdc  12215  fisumrev2  12229  fsum2mul  12236  fsum00  12245  telfsumo  12249  fsumparts  12253  iserabs  12258  cvgratnnlemabsle  12310  cvgratnn  12314  cvgratz  12315  mertenslemub  12317  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  clim2prod  12322  clim2divap  12323  prodfap0  12328  prodfrecap  12329  prodeq2  12340  fproddccvg  12355  prodrbdclem2  12356  prodmodc  12361  zproddc  12362  fprodf1o  12371  fprodssdc  12373  fprodunsn  12387  fprodcllem  12389  fprodabs  12399  fprodeq0  12400  fprodmodd  12424  eftlcvg  12470  negdvdsb  12590  dvdsnegb  12591  fsumdvds  12625  dvdsext  12638  addmodlteqALT  12642  nno  12689  gcdsupex  12750  gcdsupcl  12751  bezoutlembz  12797  dvdssq  12824  eucalgf  12849  dvdslcm  12863  lcmledvds  12864  lcmeq0  12865  lcmcl  12866  lcmdvds  12873  lcmgcdeq  12877  divgcdcoprmex  12896  isprm5lem  12936  phibndlem  13014  phiprmpw  13020  pc2dvds  13129  pcmpt  13142  prmpwdvds  13154  1arith  13166  4sqleminfi  13196  ballotfilemic  13299  ballotfilem1c  13300  ballotfilemsv  13302  ballotfilemsima  13308  ctiunctlemf  13378  ctiunct  13380  grpinva  13755  grprida  13756  sgrppropd  13777  mndpropd  13802  mhmpropd  13822  0mhm  13842  resmhm2  13844  resmhm2b  13845  grplcan  13916  mulgval  13974  mulgnn0z  14001  mulgnndir  14003  mulgnn0dir  14004  issubg2m  14041  issubg4m  14045  subgintm  14050  ghmf1  14125  gzsummhm  14194  gsumressfi  14216  prdssgrpd  14240  prdsidlem  14242  prdsmndd  14243  srglmhm  14346  srgrmhm  14347  ringpropd  14392  crngpropd  14393  ringlghm  14415  ringrghm  14416  mulgass3  14440  issubrng2  14567  subrngpropd  14573  issubrg2  14598  subrgintm  14600  subrgpropd  14610  rhmpropd  14611  unitrrg  14625  lmodprop2d  14734  islss3  14765  lssintclm  14770  qusrhm  14914  issubassa3  15061  opnssneib  15306  neissex  15315  tgrest  15319  iscnp3  15353  cnpnei  15369  cnrest  15385  tx1cn  15419  txcnp  15421  elbl3ps  15544  elbl3  15545  blininf  15574  blssexps  15579  blssex  15580  blpnfctr  15589  mopni2  15633  blsscls2  15643  metss  15644  bdmet  15652  metrest  15656  metcn  15664  txmetcn  15669  bl2ioo  15700  ivthinclemlr  15787  ivthinclemur  15789  dvcj  15859  dvfre  15860  elplyd  15891  plyaddlem1  15897  plymullem1  15898  plymullem  15900  plycolemc  15908  plycjlemc  15910  coseq0q4123  15985  abssinper  15997  fsumdvdsmul  16204  ppiqub  16212  bposlem5  16234  lgsval2lem  16248  lgsval4lem  16249  lgsneg  16262  lgsmod  16264  lgsdir2  16271  lgsdir  16273  lgsne0  16276  lgssq  16278  lgsquadlem1  16315  usgredg2vlem2  16583  clwwlkccat  16761  clwwlknonex2lem2  16798  subctctexmid  17149  cvgcmp2n  17201  iswomninnlem  17218  nconstwlpo  17235