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

Theorem mpid 44
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 43 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  49  pm2.43a  54  embantd  59  mtord  693  mpan2d  710  ceqsalt  3259  rspcimdv  3341  riotass2  6678  peano5  7131  oeordi  7712  isf34lem4  9237  domtriomlem  9302  axcclem  9317  ssnn0fi  12824  repswrevw  13579  rlimcn1  14363  climcn1  14366  climcn2  14367  dvdsgcd  15308  lcmfunsnlem2lem1  15398  coprmgcdb  15409  nprm  15448  pcqmul  15605  prmgaplem7  15808  lubun  17170  grpid  17504  psgnunilem4  17963  gexdvds  18045  scmate  20364  cayleyhamilton1  20745  uniopn  20750  tgcmp  21252  uncmp  21254  nconnsubb  21274  comppfsc  21383  kgencn2  21408  isufil2  21759  cfinufil  21779  fin1aufil  21783  flimopn  21826  cnpflf  21852  flimfnfcls  21879  fcfnei  21886  metcnp3  22392  cncfco  22757  ellimc3  23688  dvfsumrlim  23839  cxploglim  24749  nbuhgr2vtx1edgblem  26292  nbusgrvtxm1  26325  wlkp1lem6  26631  pthdlem2lem  26719  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  eupth2  27217  frgrncvvdeqlem8  27286  grpoid  27502  blocnilem  27787  htthlem  27902  nmcexi  29013  dmdbr3  29292  dmdbr4  29293  atom1d  29340  mclsax  31592  dfon2lem8  31819  nn0prpwlem  32442  nn0prpw  32443  bj-ceqsalt0  32998  bj-ceqsalt1  32999  filbcmb  33665  divrngidl  33957  lshpcmp  34593  lsat0cv  34638  atnle  34922  lpolconN  37093  ss2iundf  38268  iccpartdisj  41698  lighneallem2  41848  lighneallem3  41849  lighneallem4  41852  proththd  41856  sgoldbeven3prm  41996  bgoldbtbndlem2  42019  upgrwlkupwlk  42046  lindslinindsimp1  42571  nn0sumshdiglemA  42738  setrec1lem4  42762
  Copyright terms: Public domain W3C validator