ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  adantlr Unicode version

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  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
adantlr  |-  ( ( ( ph  /\  th )  /\  ps )  ->  ch )

Proof of Theorem adantlr
StepHypRef Expression
1 simpl 108 . 2  |-  ( (
ph  /\  th )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 281 1  |-  ( ( ( ph  /\  th )  /\  ps )  ->  ch )
Colors of variables: wff set class
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  3ad2antl1  1128  3ad2antl2  1129  ad4ant124  1179  3adant1r  1194  bilukdc  1359  intab  3770  pofun  4204  ralxfrd  4353  rexxfrd  4354  ordtri2or2exmidlem  4411  wessep  4462  poinxp  4578  relop  4659  fun11iun  5356  ssimaex  5450  fndmdif  5493  fconst2g  5603  foeqcnvco  5659  f1eqcocnv  5660  isocnv  5680  isocnv2  5681  riota2df  5718  grprinvd  5934  grpridd  5935  f1o2ndf1  6093  tfr1onlembacc  6207  tfr1onlemaccex  6213  tfr1onlemres  6214  tfrcllembacc  6220  tfrcllemaccex  6226  tfrcllemres  6227  tfrcldm  6228  tfrcl  6229  xpdom2  6693  fimax2gtrilemstep  6762  xpfi  6786  eqsupti  6851  ordiso2  6888  enumctlemm  6967  mulcanpig  7111  prarloclemlt  7269  genpdf  7284  genpdisj  7299  addnqprl  7305  addnqpru  7306  addlocpr  7312  prmuloc  7342  mulnqprl  7344  mulnqpru  7345  mullocpr  7347  ltpopr  7371  ltsopr  7372  ltaddpr  7373  ltexprlemdisj  7382  ltexprlemloc  7383  ltexprlemru  7388  addcanprleml  7390  addcanprlemu  7391  ltaprg  7395  recexprlemopu  7403  recexprlemloc  7407  cauappcvgprlemladdfl  7431  cauappcvgprlemladdru  7432  caucvgsrlemcau  7569  caucvgsrlemgt1  7571  caucvgsrlemoffcau  7574  caucvgsrlemoffres  7576  suplocsrlem  7584  axcaucvglemcau  7674  axpre-suploclemres  7677  axsuploc  7805  cnegexlem1  7905  cnegexlem3  7907  cnegex  7908  addsubeq4  7945  rimul  8314  divcanap6  8446  ltmul12a  8582  lemul12b  8583  lbinf  8670  zrevaddcl  9062  nzadd  9064  zextle  9100  fzind  9124  uz11  9304  qreccl  9390  qrevaddcl  9392  irradd  9394  xrlttr  9536  xrltso  9537  xaddass  9607  xleadd1a  9611  xlt2add  9618  iccshftr  9732  iccshftl  9734  iccdil  9736  icccntr  9738  divelunit  9740  uzsubsubfz  9782  fzaddel  9794  fzrev  9819  elfzmlbp  9864  frec2uzrdg  10137  frecuzrdgtcl  10140  frecuzrdgsuc  10142  frecuzrdgdomlem  10145  frecuzrdgfunlem  10147  frecuzrdgsuctlem  10151  iseqovex  10184  seq3val  10186  seqf  10189  seq3clss  10195  seq3fveq2  10197  seq3feq2  10198  seq3feq  10200  seq3shft2  10201  ser3mono  10206  seq3split  10207  seq3caopr3  10209  seq3caopr2  10210  iseqf1olemab  10217  seq3f1olemqsumkj  10226  seq3f1olemqsumk  10227  seq3f1olemqsum  10228  seq3f1olemstep  10229  seq3f1oleml  10231  seq3id3  10235  seq3id  10236  seq3id2  10237  seq3homo  10238  seq3z  10239  seqfeq3  10240  ser3ge0  10245  expp1  10255  expnegap0  10256  expcllem  10259  mulexp  10287  expadd  10290  expaddzap  10292  expmulzap  10294  expdivap  10299  leexp1a  10303  expnlbnd  10371  bcpasc  10467  bccl  10468  hashfacen  10534  seq3coll  10540  seq3shft  10565  resqrexlemfp1  10736  sqrtdiv  10769  climshftlemg  11026  climcn1  11032  climsqz  11059  climsqz2  11060  clim2ser  11061  clim2ser2  11062  isermulc2  11064  climub  11068  serf0  11076  fsum3cvg  11101  sumrbdc  11102  summodclem3  11104  summodclem2a  11105  zsumdc  11108  fsumf1o  11114  isumss  11115  fisumss  11116  isumss2  11117  fsum3cvg2  11118  fsum3cvg3  11120  fsumcl2lem  11122  fsumcllem  11123  fsumadd  11130  fsumsplit  11131  fsumsplitsn  11134  sumsplitdc  11156  fisumrev2  11170  fsum2mul  11177  fsum00  11186  telfsumo  11190  fsumparts  11194  iserabs  11199  cvgratnnlemabsle  11251  cvgratnn  11255  cvgratz  11256  mertenslemub  11258  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  eftlcvg  11307  negdvdsb  11421  dvdsnegb  11422  dvdsext  11465  addmodlteqALT  11469  nno  11515  infssuzex  11554  gcdsupex  11558  gcdsupcl  11559  bezoutlembz  11604  dvdssq  11631  eucalgf  11648  dvdslcm  11662  lcmledvds  11663  lcmeq0  11664  lcmcl  11665  lcmdvds  11672  lcmgcdeq  11676  divgcdcoprmex  11695  phibndlem  11803  phiprmpw  11809  ctiunctlemf  11862  ctiunct  11864  opnssneib  12236  neissex  12245  tgrest  12249  iscnp3  12283  cnpnei  12299  cnrest  12315  tx1cn  12349  txcnp  12351  elbl3ps  12474  elbl3  12475  blininf  12504  blssexps  12509  blssex  12510  blpnfctr  12519  mopni2  12563  blsscls2  12573  metss  12574  bdmet  12582  metrest  12586  metcn  12594  txmetcn  12599  bl2ioo  12622  ivthinclemlr  12695  ivthinclemur  12697  dvcj  12753  dvfre  12754  coseq0q4123  12826  subctctexmid  13092  cvgcmp2n  13124
  Copyright terms: Public domain W3C validator