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

Theorem mptru 1340
Description: Eliminate T. as an antecedent. A proposition implied by T. is true. (Contributed by Mario Carneiro, 13-Mar-2014.)
Hypothesis
Ref Expression
mptru.1  |-  ( T. 
->  ph )
Assertion
Ref Expression
mptru  |-  ph

Proof of Theorem mptru
StepHypRef Expression
1 tru 1335 . 2  |- T.
2 mptru.1 . 2  |-  ( T. 
->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   T. wtru 1332
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 depends on definitions:  df-bi 116  df-tru 1334
This theorem is referenced by:  xorbi12i  1361  nfbi  1568  spime  1719  eubii  2008  nfmo  2019  mobii  2036  dvelimc  2302  ralbii  2441  rexbii  2442  nfralxy  2471  nfrexxy  2472  nfralya  2473  nfrexya  2474  nfreuxy  2605  nfsbc1  2926  nfsbc  2929  sbcbii  2968  csbeq2i  3029  nfcsb1  3034  nfcsb  3037  nfif  3500  ssbri  3972  nfbr  3974  mpteq12i  4016  ralxfr  4387  rexxfr  4389  nfiotaw  5092  nfriota  5739  nfov  5801  mpoeq123i  5834  mpoeq3ia  5836  disjsnxp  6134  tfri1  6262  eqer  6461  0er  6463  ecopover  6527  ecopoverg  6530  nfixpxy  6611  en2i  6664  en3i  6665  ener  6673  ensymb  6674  entr  6678  djuf1olem  6938  omp1eomlem  6979  ltsopi  7135  ltsonq  7213  enq0er  7250  ltpopr  7410  ltposr  7578  axcnex  7674  axaddf  7683  axmulf  7684  ltso  7849  nfneg  7966  negiso  8720  sup3exmid  8722  xrltso  9589  frecfzennn  10206  frechashgf1o  10208  0tonninf  10219  1tonninf  10220  facnn  10480  fac0  10481  fac1  10482  cnrecnv  10689  cau3  10894  xrnegiso  11038  sum0  11164  trireciplem  11276  trirecip  11277  ege2le3  11384  oddpwdc  11859  ennnfonelem1  11927  ennnfonelemhf1o  11933  strnfvn  11990  strslss  12016  txswaphmeolem  12499  divcnap  12734  elcncf1ii  12746  cnrehmeocntop  12772  dvid  12841  dveflem  12865  dvef  12866  sincn  12868  coscn  12869  cosz12  12871  sincos6thpi  12933  bj-sbimeh  12993  bdnthALT  13047  isomninnlem  13239  taupi  13253
  Copyright terms: Public domain W3C validator