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

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

Proof of Theorem simplrl
StepHypRef Expression
1 simpl 108 . 2 ((𝜓𝜒) → 𝜓)
21ad2antlr 480 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:  rmob  2973  disjiun  3894  f1imass  5643  riota5f  5722  tfrexlem  6199  tfrcl  6229  nnsucuniel  6359  nntr2  6367  fopwdom  6698  fidceq  6731  fisbth  6745  fientri3  6771  unsnfidcex  6776  undifdc  6780  iunfidisj  6802  fiuni  6834  ordiso2  6888  acfun  7031  ccfunen  7047  addcmpblnq  7143  mulcmpblnq  7144  ordpipqqs  7150  addcmpblnq0  7219  mulcmpblnq0  7220  prml  7253  addlocpr  7312  prmuloc  7342  mullocpr  7347  ltexprlemopl  7377  ltexprlemopu  7379  ltexprlemloc  7383  ltexprlemrl  7386  ltexprlemru  7388  addcanprleml  7390  addcanprlemu  7391  aptiprleml  7415  ltmprr  7418  cauappcvgprlemopl  7422  cauappcvgprlemopu  7424  cauappcvgprlemloc  7428  caucvgprlemopl  7445  caucvgprlemopu  7447  caucvgprlemloc  7451  caucvgprprlemopu  7475  caucvgprprlemloc  7479  caucvgprprlemexbt  7482  caucvgprprlemaddq  7484  suplocexprlemrl  7493  suplocexprlemdisj  7496  suplocexprlemloc  7497  suplocexprlemub  7499  addcmpblnr  7515  mulcmpblnrlemg  7516  mulcmpblnr  7517  ltsrprg  7523  mulgt0sr  7554  caucvgsrlemgt1  7571  suplocsrlemb  7582  axmulcl  7642  axcaucvglemres  7675  axpre-suploclemres  7677  axpre-suploc  7678  cnegexlem1  7905  negeu  7921  add20  8204  apreap  8316  cru  8331  apsym  8335  apcotr  8336  apadd1  8337  apneg  8340  mulext1  8341  mulge0  8348  mulap0  8382  divdivdivap  8440  prodgt0  8574  ltmul12a  8582  lt2mul2div  8601  ledivdiv  8612  lediv12a  8616  qapne  9387  xleadd1a  9611  ixxss12  9644  elfz0ubfz0  9857  qtri3or  9975  exbtwnzlemstep  9980  exbtwnzlemex  9982  exbtwnz  9983  rebtwn2zlemstep  9985  rebtwn2z  9987  btwnzge0  10028  iseqf1olemqf1o  10221  mulexpzap  10288  leexp1a  10303  hashen  10485  fihashdom  10504  hashun  10506  cjap  10633  cvg1nlemres  10712  rsqrmo  10754  abslt  10815  abs3lem  10838  cau3lem  10841  rexanre  10947  xrmaxltsup  10982  climcau  11071  sumeq2  11083  summodc  11107  fisumss  11116  fsum2d  11159  fsumabs  11189  fsumiun  11201  eirrap  11396  divalglemeunn  11530  divalglemeuneg  11532  bezoutlemnewy  11596  bezoutlemstep  11597  bezoutlemmain  11598  bezoutlembi  11605  bezoutlemeu  11607  qredeu  11690  pw2dvdseu  11757  sqrt2irrap  11769  ennnfonelemg  11827  ennnfonelemrnh  11840  ctiunctlemfo  11863  restbasg  12248  cnpnei  12299  cnptoprest2  12320  cnpdis  12322  lmtopcnp  12330  txcnp  12351  ismet2  12434  blininf  12504  metss2lem  12577  xmettxlem  12589  xmettx  12590  metcnp  12592  metcnpi3  12597  addcncntoplem  12631  fsumcncntop  12636  mulc1cncf  12656  cncfco  12658  mulcncf  12671  dedekindeulemuub  12675  dedekindeu  12681  dedekindicclemuub  12684  ivthinclemloc  12699  ivthinc  12701  limcimo  12714  limccnp2cntop  12726  dveflem  12766  qdencn  13118
  Copyright terms: Public domain W3C validator