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

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

Proof of Theorem simprll
StepHypRef Expression
1 simpl 108 . 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  mpo0  5841  eroveu  6520  sbthlemi6  6850  sbthlemi8  6852  addcmpblnq  7187  mulcmpblnq  7188  ordpipqqs  7194  addcmpblnq0  7263  mulcmpblnq0  7264  nnnq0lem1  7266  prarloclemcalc  7322  addlocpr  7356  distrlem4prl  7404  distrlem4pru  7405  ltpopr  7415  addcmpblnr  7559  mulcmpblnrlemg  7560  mulcmpblnr  7561  prsrlem1  7562  ltsrprg  7567  apreap  8361  apreim  8377  divdivdivap  8485  divmuleqap  8489  divadddivap  8499  divsubdivap  8500  ledivdiv  8660  lediv12a  8664  exbtwnz  10040  seq3caopr  10268  leexp2r  10359  zfz1iso  10596  recvguniq  10779  rsqrmo  10811  summodclem2  11163  prodmodc  11359  qredeu  11789  pw2dvdseu  11857  epttop  12273  txdis1cn  12461  metequiv2  12679  mulc1cncf  12759  cncfmptc  12765  cncfmptid  12766  addccncf  12769  negcncf  12771  dedekindicclemicc  12793
  Copyright terms: Public domain W3C validator