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

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

Proof of Theorem simprrl
StepHypRef Expression
1 simpl 108 . 2 ((𝜒𝜃) → 𝜒)
21ad2antll 482 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:  dn1dc  944  imain  5205  grpridd  5967  tfrlemisucaccv  6222  tfrexlem  6231  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  eroveu  6520  addcmpblnq  7182  mulcmpblnq  7183  ordpipqqs  7189  nqnq0pi  7253  addcmpblnq0  7258  mulcmpblnq0  7259  prarloclemcalc  7317  prarloc  7318  nqpru  7367  mullocpr  7386  distrlem4prl  7399  distrlem4pru  7400  ltprordil  7404  ltexprlemm  7415  ltexprlemopu  7418  ltexprlemupu  7419  ltexprlemru  7427  cauappcvgprlemopl  7461  cauappcvgprlem2  7475  caucvgprlemopl  7484  caucvgprlem2  7495  caucvgprprlemexbt  7521  caucvgprprlem2  7525  suplocexprlemloc  7536  suplocexprlemub  7538  suplocexprlemlub  7539  addcmpblnr  7554  mulcmpblnrlemg  7555  mulcmpblnr  7556  prsrlem1  7557  ltsrprg  7562  axmulcl  7681  ltmul1  8361  divdivdivap  8480  divmuleqap  8484  divsubdivap  8495  lt2mul2div  8644  ledivdiv  8655  lediv12a  8659  ssfzo12bi  10009  exbtwnz  10035  qbtwnre  10041  ioom  10045  seq3caopr  10263  leexp2r  10354  hashunlem  10557  recvguniq  10774  rsqrmo  10806  fsum2dlemstep  11210  expcnvre  11279  bezout  11706  qredeu  11785  pw2dvdseu  11853  oddpwdclemdvds  11855  neiint  12324  restbasg  12347  iscnp4  12397  cnpnei  12398  cnptopco  12401  blssps  12606  blss  12607  metequiv2  12675  xmetxpbl  12687  suplociccex  12782  dedekindicc  12790  limcimolemlt  12812
  Copyright terms: Public domain W3C validator