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

Theorem simprl 520
Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
Assertion
Ref Expression
simprl ((𝜑 ∧ (𝜓𝜒)) → 𝜓)

Proof of Theorem simprl
StepHypRef Expression
1 id 19 . 2 (𝜓𝜓)
21ad2antrl 481 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜓)
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:  simp1rl  1046  simp2rl  1050  simp3rl  1054  rmob  3001  disjiun  3924  reg3exmidlemwe  4493  0xp  4619  imainss  4954  fvmptt  5512  fcof1o  5690  isotr  5717  riota5f  5754  ovmpodf  5902  grprinvlem  5965  grpridd  5967  unielxp  6072  fnmpoovd  6112  1stconst  6118  2ndconst  6119  cnvf1olem  6121  tfrlemi14d  6230  tfrexlem  6231  tfr1onlemres  6246  tfrcllemres  6259  tfrcldm  6260  frecabcl  6296  nnaordi  6404  swoer  6457  qliftfun  6511  ecopovsymg  6528  th3qlem1  6531  mapen  6740  mapxpen  6742  fidifsnen  6764  fisbth  6777  findcard2d  6785  findcard2sd  6786  diffisn  6787  diffifi  6788  ac6sfi  6792  fimax2gtri  6795  fientri3  6803  nnwetri  6804  unsnfi  6807  unsnfidcex  6808  unsnfidcel  6809  fisseneq  6820  fidcenumlemrk  6842  fidcenumlemr  6843  isbth  6855  ordiso2  6920  difinfsnlem  6984  difinfinf  6986  ctmlemr  6993  ctssdccl  6996  fodjum  7018  fodju0  7019  omniwomnimkv  7039  exmidfodomrlemrALT  7066  cc1  7087  cc2lem  7088  cc3  7090  cc4f  7091  cc4n  7093  dfplpq2  7176  dfmpq2  7177  mulpipqqs  7195  distrnqg  7209  ltexnqq  7230  subhalfnqq  7236  distrnq0  7281  prarloclemup  7317  prarloclem3  7319  prarloc  7325  genplt2i  7332  nqprl  7373  nqpru  7374  prmuloc  7388  mullocpr  7393  distrlem4prl  7406  distrlem4pru  7407  ltaddpr  7419  ltexprlemopl  7423  ltexprlemlol  7424  ltexprlemopu  7425  ltexprlemupu  7426  ltexprlemrl  7432  ltexprlemru  7434  addcanprleml  7436  addcanprlemu  7437  ltaprlem  7440  ltaprg  7441  prplnqu  7442  addextpr  7443  recexprlemdisj  7452  recexprlemloc  7453  recexprlem1ssl  7455  aptiprleml  7461  aptiprlemu  7462  ltmprr  7464  archpr  7465  cauappcvgprlemopl  7468  cauappcvgprlemopu  7470  cauappcvgprlemdisj  7473  cauappcvgprlemloc  7474  cauappcvgprlem1  7481  cauappcvgprlem2  7482  cauappcvgprlemlim  7483  caucvgprlemnkj  7488  caucvgprlemopl  7491  caucvgprlemopu  7493  caucvgprlemdisj  7496  caucvgprlemloc  7497  caucvgprlem2  7502  caucvgprprlemnkltj  7511  caucvgprprlemnkeqj  7512  caucvgprprlemnjltk  7513  caucvgprprlemmu  7517  caucvgprprlemopl  7519  caucvgprprlemopu  7521  caucvgprprlemdisj  7524  caucvgprprlemloc  7525  caucvgprprlemexbt  7528  caucvgprprlemaddq  7530  caucvgprprlem2  7532  suplocexprlemrl  7539  suplocexprlemmu  7540  suplocexprlemru  7541  suplocexprlemdisj  7542  suplocexprlemloc  7543  suplocexprlemex  7544  suplocexprlemub  7545  suplocexprlemlub  7546  recexgt0sr  7595  mulgt0sr  7600  prsrriota  7610  caucvgsrlemoffres  7622  suplocsrlem  7630  cnm  7654  addcnsr  7656  mulcnsr  7657  mulcnsrec  7665  axaddcl  7686  axmulcl  7688  axmulcom  7693  rereceu  7711  recriota  7712  axcaucvglemres  7721  axpre-suploclemres  7723  lelttr  7866  ltletr  7867  readdcan  7916  addcan  7956  addcan2  7957  addsub4  8019  ltadd2  8195  le2add  8220  lt2add  8221  lt2sub  8236  le2sub  8237  eqord1  8259  rimul  8361  rereim  8362  ltmul1  8368  apreim  8379  mulreim  8380  apcotr  8383  apadd1  8384  addext  8386  apneg  8387  mulext1  8388  mulext  8390  ltleap  8408  aprcl  8422  mulap0  8429  mulcanapd  8436  receuap  8444  rec11ap  8484  rec11rap  8485  divdivdivap  8487  ddcanap  8500  divadddivap  8501  conjmulap  8503  subrecap  8612  prodgt0gt0  8623  prodge0  8626  ltmul12a  8632  lemulge11  8638  lt2mul2div  8651  ltrec  8655  lerec  8656  lt2msq  8658  lerec2  8661  le2msq  8673  msq11  8674  ledivp1  8675  mulle0r  8716  suprzclex  9163  peano5uzti  9173  supinfneg  9404  infsupneg  9405  qapne  9445  xrlelttr  9603  xrltletr  9604  xrre  9617  xaddge0  9675  xle2add  9676  xlt2add  9677  divelunit  9799  fzass4  9856  fzocatel  9990  exbtwnzlemex  10041  rebtwn2z  10046  qbtwnre  10048  modqid  10136  modqcyc  10146  modqaddabs  10149  modqaddmod  10150  mulqaddmodid  10151  modqadd2mod  10161  modqltm1p1mod  10163  modqsubmod  10169  modqsubmodmod  10170  modqmulmod  10176  modqmulmodr  10177  modqaddmulmod  10178  modqsubdir  10180  frec2uzisod  10194  iseqovex  10243  seqvalcd  10246  seqf  10248  seqovcd  10250  seq3fveq2  10256  seq3shft2  10260  monoord  10263  seq3split  10266  iseqf1olemnab  10275  seq3id2  10296  seq3distr  10300  expcl2lemap  10319  expnegzap  10341  ltexp2a  10359  le2sq2  10382  nn0opth2  10484  bcval5  10523  hashcl  10541  hashen  10544  fihashdom  10563  hashunlem  10564  hashun  10565  fimaxq  10587  zfz1isolem1  10597  zfz1iso  10598  cvg1nlemres  10771  cvg1n  10772  recvguniq  10781  resqrexlemp1rp  10792  resqrexlemoverl  10807  resqrexlemglsq  10808  resqrexlemex  10811  sqrtmul  10821  sqrtsq  10830  absexpzap  10866  absle  10875  abs3lem  10897  amgm2  10904  maxleastlt  11001  maxltsup  11004  fimaxre2  11012  xrmaxleastlt  11039  xrmaxltsup  11041  xrmaxaddlem  11043  climcn2  11092  addcn2  11093  mulcn2  11095  reccn2ap  11096  climcau  11130  summodclem2  11165  summodc  11166  fsumf1o  11173  fisumss  11175  fsum3cvg3  11179  fsumcl2lem  11181  fsumadd  11189  fsum2dlemstep  11217  mptfzshft  11225  fsumrev  11226  fsummulc2  11231  modfsummod  11241  fsumrelem  11254  binom  11267  cvgratnn  11314  mertenslemub  11317  prodmodc  11361  efcllem  11379  tanaddaplem  11458  dvdsval2  11509  moddvds  11515  dvdsabseq  11558  dvdsflip  11562  oexpneg  11587  fldivndvdslt  11645  zsupcllemstep  11651  zssinfcl  11654  bezoutlemnewy  11697  bezoutlemstep  11698  bezoutlemeu  11708  dfgcd3  11711  bezout  11712  dvdsmulgcd  11726  bezoutr  11733  ialgrlem1st  11736  lcmgcdlem  11771  coprmdvds2  11787  qredeu  11791  rpdvds  11793  isprm6  11838  pw2dvdslemn  11856  nonsq  11898  crth  11913  ennnfonelemg  11929  ennnfonelemex  11940  ennnfonelemrnh  11942  ennnfonelemrn  11945  ennnfonelemdm  11946  ennnfonelemnn0  11948  ennnfonelemim  11950  ennnfone  11951  ctinfomlemom  11953  ctinf  11956  ctiunctlemfo  11965  isstruct2r  11986  setscom  12015  epttop  12275  topssnei  12347  restbasg  12353  restopnb  12366  cnfval  12379  cnpfval  12380  iscnp4  12403  cnpnei  12404  cnptopco  12407  cncnp  12415  cnrest2  12421  cnptoprest  12424  cnptoprest2  12425  lmss  12431  lmtopcnp  12435  neitx  12453  txcnp  12456  txrest  12461  txdis  12462  txlm  12464  cnmpt21  12476  imasnopn  12484  xmetres2  12564  blvalps  12573  blval  12574  bl2in  12588  blhalf  12593  blssps  12612  blss  12613  blssexps  12614  blssex  12615  ssblex  12616  blin2  12617  metss2lem  12682  bdmetval  12685  bdmopn  12689  metrest  12691  xmetxp  12692  xmetxpbl  12693  xmettx  12695  metcnp3  12696  txmetcnp  12703  addcncntoplem  12736  elcncf2  12746  mulc1cncf  12761  cncfco  12763  cncfmet  12764  mulcncf  12776  dedekindeulemub  12781  dedekindeulemloc  12782  dedekindeulemlu  12784  dedekindeu  12786  suplociccex  12788  dedekindicclemub  12790  dedekindicclemloc  12791  dedekindicclemlu  12793  dedekindicc  12796  ivthinclemlopn  12799  ivthinclemuopn  12801  ivthdec  12807  limcimolemlt  12818  limcimo  12819  cnplimccntop  12824  limccnp2lem  12830  limccnp2cntop  12831  dvfvalap  12835  dveflem  12872  reeff1olem  12877  reeff1oleme  12878  eflt  12881  sin0pilem2  12887  pilem3  12888  ptolemy  12929  ioocosf1o  12959  cxplt  13017  cxple  13018  cxplt3  13021  nnti  13298  pwtrufal  13299  pwf1oexmid  13301  sssneq  13304  qdencn  13331  cvgcmp2n  13337  trilpolemlt1  13343  trirec0  13346  trirec0xor  13347  supfz  13355  inffz  13356
  Copyright terms: Public domain W3C validator