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

Theorem simplrl 502
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simplrl (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜓)

Proof of Theorem simplrl
StepHypRef Expression
1 simpl 107 . 2 ((𝜓𝜒) → 𝜓)
21ad2antlr 473 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:  rmob  2907  f1imass  5445  riota5f  5523  tfrexlem  5983  tfrcl  6013  nnsucuniel  6139  fopwdom  6380  fidceq  6404  fisbth  6417  fientri3  6435  unsnfidcex  6440  undiffi  6443  ordiso2  6505  addcmpblnq  6619  mulcmpblnq  6620  ordpipqqs  6626  addcmpblnq0  6695  mulcmpblnq0  6696  prml  6729  addlocpr  6788  prmuloc  6818  mullocpr  6823  ltexprlemopl  6853  ltexprlemopu  6855  ltexprlemloc  6859  ltexprlemrl  6862  ltexprlemru  6864  addcanprleml  6866  addcanprlemu  6867  aptiprleml  6891  ltmprr  6894  cauappcvgprlemopl  6898  cauappcvgprlemopu  6900  cauappcvgprlemloc  6904  caucvgprlemopl  6921  caucvgprlemopu  6923  caucvgprlemloc  6927  caucvgprprlemopu  6951  caucvgprprlemloc  6955  caucvgprprlemexbt  6958  caucvgprprlemaddq  6960  addcmpblnr  6978  mulcmpblnrlemg  6979  mulcmpblnr  6980  ltsrprg  6986  mulgt0sr  7016  caucvgsrlemgt1  7033  axmulcl  7096  axcaucvglemres  7127  cnegexlem1  7350  negeu  7366  add20  7645  apreap  7754  cru  7769  apsym  7773  apcotr  7774  apadd1  7775  apneg  7778  mulext1  7779  mulge0  7786  mulap0  7811  divdivdivap  7868  prodgt0  7997  ltmul12a  8005  lt2mul2div  8024  ledivdiv  8035  lediv12a  8039  qapne  8805  ixxss12  9005  elfz0ubfz0  9213  qtri3or  9329  exbtwnzlemstep  9334  exbtwnzlemex  9336  exbtwnz  9337  rebtwn2zlemstep  9339  rebtwn2z  9341  btwnzge0  9382  expivallem  9574  mulexpzap  9613  leexp1a  9628  sizeen  9808  sizedom  9827  sizeun  9829  cjap  9931  cvg1nlemres  10009  rsqrmo  10051  abslt  10112  abs3lem  10135  cau3lem  10138  rexanre  10244  climcau  10322  sumeq2d  10334  sumeq2  10335  divalglemeunn  10465  divalglemeuneg  10467  bezoutlemnewy  10529  bezoutlemstep  10530  bezoutlemmain  10531  bezoutlembi  10538  bezoutlemeu  10540  qredeu  10623  pw2dvdseu  10690  sqrt2irrap  10702  qdencn  10943
  Copyright terms: Public domain W3C validator