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

Theorem adantlr 446
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
StepHypRef Expression
1 simpl 102 . 2 ((𝜑𝜃) → 𝜑)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan 267 1 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  ad2antrr  457  ad2ant2r  478  ad2ant2rl  480  3ad2antl1  1066  3ad2antl2  1067  3adant1r  1128  bilukdc  1287  intab  3644  pofun  4049  ralxfrd  4194  rexxfrd  4195  ordtri2or2exmidlem  4251  wessep  4302  poinxp  4409  relop  4486  fun11iun  5147  ssimaex  5234  fndmdif  5272  fconst2g  5376  foeqcnvco  5430  f1eqcocnv  5431  isocnv  5451  isocnv2  5452  riota2df  5488  grprinvd  5696  grpridd  5697  f1o2ndf1  5849  xpdom2  6305  ordiso2  6357  mulcanpig  6433  prarloclemlt  6591  genpdf  6606  genpdisj  6621  addnqprl  6627  addnqpru  6628  addlocpr  6634  prmuloc  6664  mulnqprl  6666  mulnqpru  6667  mullocpr  6669  ltpopr  6693  ltsopr  6694  ltaddpr  6695  ltexprlemdisj  6704  ltexprlemloc  6705  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  ltaprg  6717  recexprlemopu  6725  recexprlemloc  6729  cauappcvgprlemladdfl  6753  cauappcvgprlemladdru  6754  caucvgsrlemcau  6877  caucvgsrlemgt1  6879  caucvgsrlemoffcau  6882  caucvgsrlemoffres  6884  axcaucvglemcau  6972  cnegexlem1  7186  cnegexlem3  7188  cnegex  7189  addsubeq4  7226  rimul  7576  divcanap6  7695  ltmul12a  7826  lemul12b  7827  zrevaddcl  8295  zextle  8331  fzind  8353  uz11  8495  qreccl  8576  qrevaddcl  8578  irradd  8580  xrlttr  8716  xrltso  8717  iccshftr  8862  iccshftl  8864  iccdil  8866  icccntr  8868  divelunit  8870  uzsubsubfz  8911  fzaddel  8922  fzrev  8946  elfzmlbp  8990  frec2uzrdg  9195  frecuzrdgfn  9198  frecuzrdgcl  9199  frecuzrdgsuc  9201  iseqovex  9219  iseqval  9220  iseqf  9224  iseqss  9226  iseqfveq2  9228  iseqfeq2  9229  iseqfeq  9231  iseqshft2  9232  isermono  9237  iseqsplit  9238  iseqcaopr3  9240  iseqcaopr2  9241  iseqid3s  9246  iseqid  9247  iseqhomo  9248  expivallem  9256  expival  9257  expp1  9262  expnegap0  9263  expcllem  9266  mulexp  9294  expadd  9297  expaddzap  9299  expmulzap  9301  expdivap  9305  leexp1a  9309  expnlbnd  9373  resqrexlemfp1  9607  sqrtdiv  9640  climshftlemg  9823  climcn1  9829  climsqz  9855  climsqz2  9856  clim2iser  9857  clim2iser2  9858  iisermulc2  9860  iserile  9862  climub  9864  climserile  9865  serif0  9871
  Copyright terms: Public domain W3C validator