Theorem adantlr 469

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  480  ad2ant2r  501  ad2ant2rl  503  adantl3r  504  ad4ant14  506  ad4ant24  508  ad5ant13  511  ad5ant14  512  ad5ant15  513  3ad2antl1  1149  3ad2antl2  1150  ad4ant124  1206  3adant1r  1221  bilukdc  1386  intab  3853  pofun  4290  ralxfrd  4440  rexxfrd  4441  ordtri2or2exmidlem  4503  wessep  4555  poinxp  4673  relop  4754  fun11iun  5453  ssimaex  5547  fndmdif  5590  fconst2g  5700  foeqcnvco  5758  f1eqcocnv  5759  isocnv  5779  isocnv2  5780  riota2df  5818  f1o2ndf1  6196  tfr1onlembacc  6310  tfr1onlemaccex  6316  tfr1onlemres  6317  tfrcllembacc  6323  tfrcllemaccex  6329  tfrcllemres  6330  tfrcldm  6331  tfrcl  6332  xpdom2  6797  fimax2gtrilemstep  6866  xpfi  6895  eqsupti  6961  ordiso2  7000  enumctlemm  7079  enwomnilem  7133  cc2lem  7207  mulcanpig  7276  prarloclemlt  7434  genpdf  7449  genpdisj  7464  addnqprl  7470  addnqpru  7471  addlocpr  7477  prmuloc  7507  mulnqprl  7509  mulnqpru  7510  mullocpr  7512  ltpopr  7536  ltsopr  7537  ltaddpr  7538  ltexprlemdisj  7547  ltexprlemloc  7548  ltexprlemru  7553  addcanprleml  7555  addcanprlemu  7556  ltaprg  7560  recexprlemopu  7568  recexprlemloc  7572  cauappcvgprlemladdfl  7596  cauappcvgprlemladdru  7597  caucvgsrlemcau  7734  caucvgsrlemgt1  7736  caucvgsrlemoffcau  7739  caucvgsrlemoffres  7741  suplocsrlem  7749  axcaucvglemcau  7839  axpre-suploclemres  7842  axsuploc  7971  cnegexlem1  8073  cnegexlem3  8075  cnegex  8076  addsubeq4  8113  rimul  8483  divcanap6  8615  ltmul12a  8755  lemul12b  8756  lbinf  8843  zrevaddcl  9241  nzadd  9243  zextle  9282  fzind  9306  uz11  9488  infregelbex  9536  qreccl  9580  qrevaddcl  9582  irradd  9584  xrlttr  9731  xrltso  9732  xaddass  9805  xleadd1a  9809  xlt2add  9816  iccshftr  9930  iccshftl  9932  iccdil  9934  icccntr  9936  divelunit  9938  uzsubsubfz  9982  fzaddel  9994  fzrev  10019  elfzmlbp  10067  frec2uzrdg  10344  frecuzrdgtcl  10347  frecuzrdgsuc  10349  frecuzrdgdomlem  10352  frecuzrdgfunlem  10354  frecuzrdgsuctlem  10358  iseqovex  10391  seq3val  10393  seqf  10396  seq3clss  10402  seq3fveq2  10404  seq3feq2  10405  seq3feq  10407  seq3shft2  10408  ser3mono  10413  seq3split  10414  seq3caopr3  10416  seq3caopr2  10417  iseqf1olemab  10424  seq3f1olemqsumkj  10433  seq3f1olemqsumk  10434  seq3f1olemqsum  10435  seq3f1olemstep  10436  seq3f1oleml  10438  seq3id3  10442  seq3id  10443  seq3id2  10444  seq3homo  10445  seq3z  10446  seqfeq3  10447  ser3ge0  10452  expp1  10462  expnegap0  10463  expcllem  10466  mulexp  10494  expadd  10497  expaddzap  10499  expmulzap  10501  expdivap  10506  leexp1a  10510  expnlbnd  10579  bcpasc  10679  bccl  10680  hashfacen  10749  seq3coll  10755  seq3shft  10780  resqrexlemfp1  10951  sqrtdiv  10984  climshftlemg  11243  climcn1  11249  climsqz  11276  climsqz2  11277  clim2ser  11278  clim2ser2  11279  isermulc2  11281  climub  11285  serf0  11293  fsum3cvg  11319  sumrbdc  11320  summodclem3  11321  summodclem2a  11322  zsumdc  11325  fsumf1o  11331  isumss  11332  fisumss  11333  isumss2  11334  fsum3cvg2  11335  fsum3cvg3  11337  fsumcl2lem  11339  fsumcllem  11340  fsumadd  11347  fsumsplit  11348  fsumsplitsn  11351  sumsplitdc  11373  fisumrev2  11387  fsum2mul  11394  fsum00  11403  telfsumo  11407  fsumparts  11411  iserabs  11416  cvgratnnlemabsle  11468  cvgratnn  11472  cvgratz  11473  mertenslemub  11475  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  clim2prod  11480  clim2divap  11481  prodfap0  11486  prodfrecap  11487  prodeq2  11498  fproddccvg  11513  prodrbdclem2  11514  prodmodc  11519  zproddc  11520  fprodf1o  11529  fprodssdc  11531  fprodunsn  11545  fprodcllem  11547  fprodabs  11557  fprodeq0  11558  fprodmodd  11582  eftlcvg  11628  negdvdsb  11747  dvdsnegb  11748  dvdsext  11793  addmodlteqALT  11797  nno  11843  infssuzex  11882  zsupssdc  11887  gcdsupex  11890  gcdsupcl  11891  bezoutlembz  11937  dvdssq  11964  eucalgf  11987  dvdslcm  12001  lcmledvds  12002  lcmeq0  12003  lcmcl  12004  lcmdvds  12011  lcmgcdeq  12015  divgcdcoprmex  12034  isprm5lem  12073  phibndlem  12148  phiprmpw  12154  pc2dvds  12261  pcmpt  12273  prmpwdvds  12285  1arith  12297  ctiunctlemf  12371  ctiunct  12373  grprinvd  12617  grpridd  12618  opnssneib  12796  neissex  12805  tgrest  12809  iscnp3  12843  cnpnei  12859  cnrest  12875  tx1cn  12909  txcnp  12911  elbl3ps  13034  elbl3  13035  blininf  13064  blssexps  13069  blssex  13070  blpnfctr  13079  mopni2  13123  blsscls2  13133  metss  13134  bdmet  13142  metrest  13146  metcn  13154  txmetcn  13159  bl2ioo  13182  ivthinclemlr  13255  ivthinclemur  13257  dvcj  13313  dvfre  13314  coseq0q4123  13395  abssinper  13407  lgsval2lem  13551  lgsval4lem  13552  lgsneg  13565  lgsmod  13567  lgsdir2  13574  lgsdir  13576  lgsne0  13579  lgssq  13581  subctctexmid  13881  cvgcmp2n  13912  iswomninnlem  13928  nconstwlpo  13944