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

Theorem simprl 483
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 459 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:  simp1rl  968  simp2rl  972  simp3rl  976  rmob  2844  0xp  4363  imainss  4682  fvmptt  5205  fcof1o  5372  isotr  5399  riota5f  5435  ovmpt2df  5574  grprinvlem  5637  grpridd  5639  unielxp  5742  1stconst  5784  2ndconst  5785  cnvf1olem  5787  tfrlemi14d  5888  tfrexlem  5889  nnaordi  6017  swoer  6070  qliftfun  6124  ecopovsymg  6141  th3qlem1  6144  dfplpq2  6338  dfmpq2  6339  mulpipqqs  6357  distrnqg  6371  ltexnqq  6391  subhalfnqq  6397  distrnq0  6441  prarloclemup  6477  prarloclem3  6479  prarloc  6485  genplt2i  6492  prmuloc  6545  mullocpr  6550  distrlem4prl  6558  distrlem4pru  6559  ltaddpr  6569  ltexprlemopl  6573  ltexprlemlol  6574  ltexprlemopu  6575  ltexprlemupu  6576  ltexprlemrl  6582  ltexprlemru  6584  addcanprleml  6586  addcanprlemu  6587  ltaprlem  6589  ltaprg  6590  addextpr  6591  recexprlemdisj  6600  recexprlemloc  6601  recexprlem1ssl  6603  aptiprleml  6609  aptiprlemu  6610  ltmprr  6612  archpr  6613  recexgt0sr  6661  mulgt0sr  6664  addcnsr  6691  mulcnsr  6692  mulcnsrec  6700  axaddcl  6710  axmulcl  6712  axmulcom  6715  lelttr  6863  ltletr  6864  readdcan  6910  addcan  6948  addcan2  6949  addsub4  7010  ltadd2  7172  le2add  7194  lt2add  7195  lt2sub  7210  le2sub  7211  rimul  7329  rereim  7330  ltmul1  7336  apreim  7347  mulreim  7348  apcotr  7351  apadd1  7352  addext  7354  apneg  7355  mulext1  7356  mulext  7358  ltleap  7373  mulap0  7377  mulcanapd  7384  receuap  7392  rec11ap  7428  rec11rap  7429  divdivdivap  7431  ddcanap  7444  divadddivap  7445  conjmulap  7447  prodgt0gt0  7558  prodge0  7561  ltmul12a  7567  lemulge11  7573  lt2mul2div  7586  ltrec  7590  lerec  7591  lt2msq  7593  lerec2  7596  le2msq  7608  msq11  7609  ledivp1  7610  peano5uzti  8082  qapne  8310  xrlelttr  8452  xrltletr  8453  xrre  8463  divelunit  8600  fzass4  8655  fzocatel  8785  frec2uzisod  8834  iseqovex  8859  iseqval  8860  iseqfveq2  8865  expivallem  8870  expcl2lemap  8881  expnegzap  8903  ltexp2a  8920  le2sq2  8942
  Copyright terms: Public domain W3C validator