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

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

Proof of Theorem simplrl
StepHypRef Expression
1 simpl 109 . 2 ((𝜓𝜒) → 𝜓)
21ad2antlr 489 1 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  rmob  3055  disjiun  3995  f1imass  5768  riota5f  5848  tfrexlem  6328  tfrcl  6358  nnsucuniel  6489  nntr2  6497  fopwdom  6829  fidceq  6862  fisbth  6876  fientri3  6907  unsnfidcex  6912  undifdc  6916  iunfidisj  6938  fiuni  6970  ordiso2  7027  acfun  7199  ccfunen  7241  addcmpblnq  7344  mulcmpblnq  7345  ordpipqqs  7351  addcmpblnq0  7420  mulcmpblnq0  7421  prml  7454  addlocpr  7513  prmuloc  7543  mullocpr  7548  ltexprlemopl  7578  ltexprlemopu  7580  ltexprlemloc  7584  ltexprlemrl  7587  ltexprlemru  7589  addcanprleml  7591  addcanprlemu  7592  aptiprleml  7616  ltmprr  7619  cauappcvgprlemopl  7623  cauappcvgprlemopu  7625  cauappcvgprlemloc  7629  caucvgprlemopl  7646  caucvgprlemopu  7648  caucvgprlemloc  7652  caucvgprprlemopu  7676  caucvgprprlemloc  7680  caucvgprprlemexbt  7683  caucvgprprlemaddq  7685  suplocexprlemrl  7694  suplocexprlemdisj  7697  suplocexprlemloc  7698  suplocexprlemub  7700  addcmpblnr  7716  mulcmpblnrlemg  7717  mulcmpblnr  7718  ltsrprg  7724  mulgt0sr  7755  caucvgsrlemgt1  7772  suplocsrlemb  7783  axmulcl  7843  axcaucvglemres  7876  axpre-suploclemres  7878  axpre-suploc  7879  cnegexlem1  8109  negeu  8125  add20  8408  apreap  8521  cru  8536  apsym  8540  apcotr  8541  apadd1  8542  apneg  8545  mulext1  8546  mulge0  8553  mulap0  8587  divdivdivap  8646  prodgt0  8785  ltmul12a  8793  lt2mul2div  8812  ledivdiv  8823  lediv12a  8827  qapne  9615  xleadd1a  9847  ixxss12  9880  elfz0ubfz0  10098  qtri3or  10216  exbtwnzlemstep  10221  exbtwnzlemex  10223  exbtwnz  10224  rebtwn2zlemstep  10226  rebtwn2z  10228  btwnzge0  10273  iseqf1olemqf1o  10466  mulexpzap  10533  leexp1a  10548  hashen  10735  fihashdom  10754  hashun  10756  cjap  10886  cvg1nlemres  10965  rsqrmo  11007  abslt  11068  abs3lem  11091  cau3lem  11094  rexanre  11200  xrmaxltsup  11237  climcau  11326  sumeq2  11338  summodc  11362  fisumss  11371  fsum2d  11414  fsumabs  11444  fsumiun  11456  prodeq2  11536  prodmodclem2  11556  fprodcl2lem  11584  fprodap0  11600  fprod2d  11602  fprodrec  11608  fprodap0f  11615  fprodle  11619  eirrap  11756  divalglemeunn  11896  divalglemeuneg  11898  bezoutlemnewy  11967  bezoutlemstep  11968  bezoutlemmain  11969  bezoutlembi  11976  bezoutlemeu  11978  qredeu  12067  isprm5lem  12111  pw2dvdseu  12138  sqrt2irrap  12150  pythagtriplem2  12236  pythagtrip  12253  pclemub  12257  pcqmul  12273  pcexp  12279  pcneg  12294  pcprmpw2  12302  pcadd  12309  prmpwdvds  12323  ennnfonelemg  12374  ennnfonelemrnh  12387  ctiunctlemfo  12410  nninfdclemf1  12423  ismndd  12717  mndpropd  12720  mhmeql  12753  mhmmnd  12856  mulgfng  12863  ringpropd  13030  dvdsrtr  13082  restbasg  13301  cnpnei  13352  cnptoprest2  13373  cnpdis  13375  lmtopcnp  13383  txcnp  13404  ismet2  13487  blininf  13557  metss2lem  13630  xmettxlem  13642  xmettx  13643  metcnp  13645  metcnpi3  13650  addcncntoplem  13684  fsumcncntop  13689  mulc1cncf  13709  cncfco  13711  mulcncf  13724  dedekindeulemuub  13728  dedekindeu  13734  dedekindicclemuub  13737  ivthinclemloc  13752  ivthinc  13754  limcimo  13767  limccnp2cntop  13779  dveflem  13820  logbgcd1irrap  14021  lgsdilem  14061  2sqlem5  14088  2sqlem9  14093  qdencn  14398  apdiff  14419
  Copyright terms: Public domain W3C validator