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

Theorem simprlr 528
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 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:  imain  5252  fcof1  5733  fliftfun  5746  sbthlemi6  6906  sbthlemi8  6908  addcmpblnq  7287  mulcmpblnq  7288  ordpipqqs  7294  enq0tr  7354  addcmpblnq0  7363  mulcmpblnq0  7364  nnnq0lem1  7366  addnq0mo  7367  mulnq0mo  7368  prarloclemcalc  7422  addlocpr  7456  distrlem4prl  7504  distrlem4pru  7505  addcmpblnr  7659  mulcmpblnrlemg  7660  mulcmpblnr  7661  prsrlem1  7662  addsrmo  7663  mulsrmo  7664  ltsrprg  7667  apreap  8462  apreim  8478  divdivdivap  8586  divsubdivap  8601  ledivdiv  8761  lediv12a  8765  exbtwnz  10150  seq3caopr  10382  leexp2r  10473  zfz1iso  10712  recvguniq  10895  rsqrmo  10927  summodclem2  11279  prodmodclem2  11474  prodmodc  11475  qredeu  11974  pw2dvdseu  12043  epttop  12501  txdis1cn  12689  metequiv2  12907  cncfmptc  12993  cncfmptid  12994  addccncf  12997  negcncf  12999  dedekindicclemicc  13021
  Copyright terms: Public domain W3C validator