MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpid Structured version   Visualization version   GIF version

Theorem mpid 43
Description: A nested modus ponens deduction. Deduction associated with mpi 20. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
mpid.1 (𝜑𝜒)
mpid.2 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
mpid (𝜑 → (𝜓𝜃))

Proof of Theorem mpid
StepHypRef Expression
1 mpid.1 . . 3 (𝜑𝜒)
21a1d 25 . 2 (𝜑 → (𝜓𝜒))
3 mpid.2 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
42, 3mpdd 42 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  mp2d  47  pm2.43a  52  embantd  57  mtord  690  mpan2d  706  ceqsalt  3201  rspcimdv  3283  riotass2  6515  peano5  6959  oeordi  7532  isf34lem4  9060  domtriomlem  9125  axcclem  9140  ssnn0fi  12604  repswrevw  13333  rlimcn1  14116  climcn1  14119  climcn2  14120  dvdsgcd  15048  lcmfunsnlem2lem1  15138  coprmgcdb  15149  nprm  15188  pcqmul  15345  prmgaplem7  15548  lubun  16895  grpid  17229  psgnunilem4  17689  gexdvds  17771  scmate  20083  cayleyhamilton1  20464  uniopn  20475  tgcmp  20962  uncmp  20964  nconsubb  20984  comppfsc  21093  kgencn2  21118  isufil2  21470  cfinufil  21490  fin1aufil  21494  flimopn  21537  cnpflf  21563  flimfnfcls  21590  fcfnei  21597  metcnp3  22103  cncfco  22466  ellimc3  23394  dvfsumrlim  23543  cxploglim  24449  constr3trllem2  25973  frgrancvvdeqlemB  26359  grpoid  26552  blocnilem  26837  htthlem  26952  nmcexi  28063  dmdbr3  28342  dmdbr4  28343  atom1d  28390  mclsax  30514  dfon2lem8  30733  nn0prpwlem  31281  nn0prpw  31282  bj-ceqsalt0  31861  bj-ceqsalt1  31862  filbcmb  32499  divrngidl  32791  lshpcmp  33087  lsat0cv  33132  atnle  33416  lpolconN  35588  ss2iundf  36764  iccpartdisj  39770  lighneallem2  39856  lighneallem3  39857  lighneallem4  39860  proththd  39864  bgoldbtbndlem2  40017  nbuhgr2vtx1edgblem  40565  nbusgrvtxm1  40599  upgr1wlkwlk  40839  1wlkp1lem6  40879  pthdlem2lem  40965  crctcsh1wlkn0lem4  41008  crctcsh1wlkn0lem5  41009  wwlks2onv  41150  eupth2  41399  frgrncvvdeqlemB  41469  lindslinindsimp1  42032  nn0sumshdiglemA  42203
  Copyright terms: Public domain W3C validator