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

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

Proof of Theorem simprlr
StepHypRef Expression
1 simpr 110 . 2 ((𝜓𝜒) → 𝜒)
21ad2antrl 490 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:  imain  5312  fcof1  5799  fliftfun  5812  sbthlemi6  6978  sbthlemi8  6980  addcmpblnq  7383  mulcmpblnq  7384  ordpipqqs  7390  enq0tr  7450  addcmpblnq0  7459  mulcmpblnq0  7460  nnnq0lem1  7462  addnq0mo  7463  mulnq0mo  7464  prarloclemcalc  7518  addlocpr  7552  distrlem4prl  7600  distrlem4pru  7601  addcmpblnr  7755  mulcmpblnrlemg  7756  mulcmpblnr  7757  prsrlem1  7758  addsrmo  7759  mulsrmo  7760  ltsrprg  7763  apreap  8561  apreim  8577  aptap  8624  divdivdivap  8687  divsubdivap  8702  ledivdiv  8864  lediv12a  8868  exbtwnz  10268  seq3caopr  10500  leexp2r  10591  zfz1iso  10838  recvguniq  11021  rsqrmo  11053  summodclem2  11407  prodmodclem2  11602  prodmodc  11603  qredeu  12114  pw2dvdseu  12185  pcadd  12356  mhmpropd  12883  grprcan  12946  isnsg3  13111  ghmpreima  13165  rngpropd  13269  ringpropd  13352  islmodd  13569  lmodprop2d  13624  lss1d  13659  epttop  13973  txdis1cn  14161  metequiv2  14379  cncfmptc  14465  cncfmptid  14466  addccncf  14469  negcncf  14471  dedekindicclemicc  14493  2sqlem5  14849  2sqlem9  14854
  Copyright terms: Public domain W3C validator