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

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

Proof of Theorem simplrr
StepHypRef Expression
1 simpr 109 . 2 ((𝜓𝜒) → 𝜒)
21ad2antlr 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:  rmob  3002  disjiun  3928  isotr  5721  riota5f  5758  tfrexlem  6235  tfrcl  6265  nnsucuniel  6395  fopwdom  6734  dif1enen  6778  fisbth  6781  fin0  6783  fin0or  6784  diffisn  6791  finexdc  6800  fientri3  6807  unfidisj  6814  undifdc  6816  ssfirab  6826  fnfi  6829  iunfidisj  6838  ordiso2  6924  difinfinf  6990  ctmlemr  6997  exmidfodomrlemr  7071  cc2lem  7094  cc3  7096  addcmpblnq  7195  mulcmpblnq  7196  ordpipqqs  7202  ltexnqq  7236  addcmpblnq0  7271  mulcmpblnq0  7272  prmu  7306  addlocpr  7364  prmuloc  7394  prmuloc2  7395  ltaddpr  7425  ltexprlemopl  7429  ltexprlemopu  7431  ltexprlemloc  7435  ltexprlemrl  7438  ltexprlemru  7440  addcanprleml  7442  addcanprlemu  7443  aptiprleml  7467  aptiprlemu  7468  ltmprr  7470  cauappcvgprlemloc  7480  archrecpr  7492  caucvgprlemloc  7503  caucvgprprlemloc  7531  caucvgprprlemexbt  7534  suplocexprlemdisj  7548  suplocexprlemloc  7549  addcmpblnr  7567  mulcmpblnrlemg  7568  mulcmpblnr  7569  ltsrprg  7575  mulgt0sr  7606  caucvgsrlemgt1  7623  suplocsrlemb  7634  axmulcl  7694  axarch  7719  axcaucvglemres  7727  axpre-suploclemres  7729  axpre-suploc  7730  readdcan  7922  cnegexlem1  7957  negeu  7973  add20  8256  apreap  8369  cru  8384  apsym  8388  apcotr  8389  apadd1  8390  apneg  8393  mulext1  8394  divdivdivap  8493  ltmul12a  8638  lemul12a  8640  lt2mul2div  8657  ledivdiv  8668  lediv12a  8672  qapne  9454  xleadd1a  9682  ixxss12  9715  ioodisj  9802  fz0fzelfz0  9931  qtri3or  10047  exbtwnzlemstep  10052  exbtwnzlemex  10054  exbtwnz  10055  rebtwn2zlemstep  10057  rebtwn2z  10059  qbtwnre  10061  btwnzge0  10100  iseqf1olemqf1o  10293  mulexpzap  10360  leexp1a  10375  expnbnd  10442  hashen  10558  fihashdom  10577  hashun  10579  zfz1iso  10612  cjap  10706  cvg1nlemres  10785  rsqrmo  10827  abs3lem  10911  cau3lem  10914  rexanre  11020  xrmaxltsup  11055  climcau  11144  sumeq2  11156  summodc  11180  fsum3cvg3  11193  fsum2d  11232  prodeq2  11354  prodmodclem2  11374  eirrap  11511  addmodlteqALT  11584  divalglemeunn  11645  divalglemeuneg  11647  zsupcllemstep  11665  bezoutlemnewy  11711  bezoutlemstep  11712  bezoutlemmain  11713  bezoutlembi  11720  bezoutlemeu  11722  rpdvds  11807  isprm6  11852  pw2dvdslemn  11870  pw2dvdseu  11873  sqrt2irrap  11885  ennnfonelemrnh  11956  ennnfonelemnn0  11962  ctinfomlemom  11967  ctiunctlemfo  11979  restbasg  12367  cnrest2  12435  cnpdis  12441  lmtopcnp  12449  txcnp  12470  txlm  12478  ismet2  12553  blininf  12623  metss2lem  12696  xmettxlem  12708  xmettx  12709  metcnp3  12710  metcnpi3  12716  addcncntoplem  12750  fsumcncntop  12755  mulcncf  12790  dedekindeulemuub  12794  dedekindeu  12800  dedekindicclemuub  12803  ivthinclemlopn  12813  ivthinclemuopn  12815  ivthinclemloc  12818  ivthinc  12820  limcimo  12833  limccnp2cntop  12845  logbgcd1irrap  13086  qdencn  13380  apdiff  13399
  Copyright terms: Public domain W3C validator