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

Theorem mp2b 8
Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.)
Hypotheses
Ref Expression
mp2b.1 𝜑
mp2b.2 (𝜑𝜓)
mp2b.3 (𝜓𝜒)
Assertion
Ref Expression
mp2b 𝜒

Proof of Theorem mp2b
StepHypRef Expression
1 mp2b.1 . . 3 𝜑
2 mp2b.2 . . 3 (𝜑𝜓)
31, 2ax-mp 5 . 2 𝜓
4 mp2b.3 . 2 (𝜓𝜒)
53, 4ax-mp 5 1 𝜒
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5
This theorem is referenced by:  eqvinc  2780  2ordpr  4407  regexmid  4418  ordsoexmid  4445  reg3exmid  4462  intasym  4891  relcoi1  5038  funres11  5163  cnvresid  5165  mpofvex  6067  df1st2  6082  df2nd2  6083  dftpos4  6126  tposf12  6132  frecabcl  6262  xp01disjl  6297  xpcomco  6686  ominf  6756  sbthlem2  6812  djuunr  6917  eldju  6919  ctssdccl  6962  ctssdclemr  6963  omct  6968  ctssexmid  6990  rec1nq  7167  halfnqq  7182  caucvgsrlemasr  7562  axresscn  7632  0re  7730  gtso  7807  cnegexlem2  7902  uzn0  9290  indstr  9337  dfioo2  9697  fnn0nninf  10150  hashinfuni  10463  hashp1i  10496  cnrecnv  10622  rexanuz  10700  xrmaxiflemcom  10958  climdm  11004  sumsnf  11118  tanvalap  11314  egt2lt3  11382  lcmgcdlem  11654  3prm  11705  sqpweven  11748  2sqpwodd  11749  qnumval  11758  qdenval  11759  xpnnen  11802  ennnfonelemhdmp1  11817  ennnfonelemss  11818  ennnfonelemnn0  11830  qnnen  11839  unct  11849  structcnvcnv  11870  setsslid  11904  tgrest  12233  lmbr2  12278  cnptoprest  12303  lmff  12313  tx1cn  12333  tx2cn  12334  cnblcld  12599  tgioo  12610  pilem1  12734  isomninnlem  13027
  Copyright terms: Public domain W3C validator