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

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

Proof of Theorem simprlr
StepHypRef Expression
1 simpr 109 . 2 ((𝜓𝜒) → 𝜒)
21ad2antrl 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:  imain  5205  fcof1  5684  fliftfun  5697  sbthlemi6  6850  sbthlemi8  6852  addcmpblnq  7187  mulcmpblnq  7188  ordpipqqs  7194  enq0tr  7254  addcmpblnq0  7263  mulcmpblnq0  7264  nnnq0lem1  7266  addnq0mo  7267  mulnq0mo  7268  prarloclemcalc  7322  addlocpr  7356  distrlem4prl  7404  distrlem4pru  7405  addcmpblnr  7559  mulcmpblnrlemg  7560  mulcmpblnr  7561  prsrlem1  7562  addsrmo  7563  mulsrmo  7564  ltsrprg  7567  apreap  8361  apreim  8377  divdivdivap  8485  divsubdivap  8500  ledivdiv  8660  lediv12a  8664  exbtwnz  10040  seq3caopr  10268  leexp2r  10359  zfz1iso  10596  recvguniq  10779  rsqrmo  10811  summodclem2  11163  prodmodclem2  11358  prodmodc  11359  qredeu  11789  pw2dvdseu  11857  epttop  12273  txdis1cn  12461  metequiv2  12679  cncfmptc  12765  cncfmptid  12766  addccncf  12769  negcncf  12771  dedekindicclemicc  12793
  Copyright terms: Public domain W3C validator