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

Theorem adantlr 461
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 107 . 2 ((𝜑𝜃) → 𝜑)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan 277 1 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  ad2antrr  472  ad2ant2r  493  ad2ant2rl  495  3ad2antl1  1101  3ad2antl2  1102  3adant1r  1163  bilukdc  1328  intab  3673  pofun  4075  ralxfrd  4220  rexxfrd  4221  ordtri2or2exmidlem  4277  wessep  4328  poinxp  4435  relop  4514  fun11iun  5178  ssimaex  5266  fndmdif  5304  fconst2g  5408  foeqcnvco  5461  f1eqcocnv  5462  isocnv  5482  isocnv2  5483  riota2df  5519  grprinvd  5727  grpridd  5728  f1o2ndf1  5880  tfr1onlembacc  5991  tfr1onlemaccex  5997  tfr1onlemres  5998  tfrcllembacc  6004  tfrcllemaccex  6010  tfrcllemres  6011  tfrcldm  6012  tfrcl  6013  xpdom2  6375  eqsupti  6468  ordiso2  6505  mulcanpig  6587  prarloclemlt  6745  genpdf  6760  genpdisj  6775  addnqprl  6781  addnqpru  6782  addlocpr  6788  prmuloc  6818  mulnqprl  6820  mulnqpru  6821  mullocpr  6823  ltpopr  6847  ltsopr  6848  ltaddpr  6849  ltexprlemdisj  6858  ltexprlemloc  6859  ltexprlemru  6864  addcanprleml  6866  addcanprlemu  6867  ltaprg  6871  recexprlemopu  6879  recexprlemloc  6883  cauappcvgprlemladdfl  6907  cauappcvgprlemladdru  6908  caucvgsrlemcau  7031  caucvgsrlemgt1  7033  caucvgsrlemoffcau  7036  caucvgsrlemoffres  7038  axcaucvglemcau  7126  cnegexlem1  7350  cnegexlem3  7352  cnegex  7353  addsubeq4  7390  rimul  7752  divcanap6  7874  ltmul12a  8005  lemul12b  8006  lbinf  8093  zrevaddcl  8482  nzadd  8484  zextle  8519  fzind  8543  uz11  8722  qreccl  8808  qrevaddcl  8810  irradd  8812  xrlttr  8946  xrltso  8947  iccshftr  9092  iccshftl  9094  iccdil  9096  icccntr  9098  divelunit  9100  uzsubsubfz  9142  fzaddel  9153  fzrev  9177  elfzmlbp  9220  frec2uzrdg  9491  frecuzrdgtcl  9494  frecuzrdgsuc  9496  frecuzrdgdomlem  9499  frecuzrdgfunlem  9501  frecuzrdgsuctlem  9505  iseqovex  9529  iseqval  9530  iseqvalt  9532  iseqfclt  9536  iseqoveq  9540  iseqss  9541  iseqsst  9542  iseqfveq2  9544  iseqfeq2  9545  iseqfeq  9547  iseqshft2  9548  isermono  9553  iseqsplit  9554  iseqcaopr3  9556  iseqcaopr2  9557  iseqid3s  9562  iseqid  9563  iseqid2  9564  iseqhomo  9565  iseqz  9566  expivallem  9574  expival  9575  expp1  9580  expnegap0  9581  expcllem  9584  mulexp  9612  expadd  9615  expaddzap  9617  expmulzap  9619  expdivap  9624  leexp1a  9628  expnlbnd  9694  bcpasc  9790  bccl  9791  resqrexlemfp1  10033  sqrtdiv  10066  climshftlemg  10279  climcn1  10285  climsqz  10311  climsqz2  10312  clim2iser  10313  clim2iser2  10314  iisermulc2  10316  iserile  10318  climub  10320  climserile  10321  serif0  10327  fisumcvg  10338  isumrb  10339  negdvdsb  10356  dvdsnegb  10357  dvdsext  10400  addmodlteqALT  10404  nno  10450  infssuzex  10489  gcdsupex  10493  gcdsupcl  10494  bezoutlembz  10537  dvdssq  10564  eucalgf  10581  dvdslcm  10595  lcmledvds  10596  lcmeq0  10597  lcmcl  10598  lcmdvds  10605  lcmgcdeq  10609  divgcdcoprmex  10628
  Copyright terms: Public domain W3C validator