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

Theorem mpcom 36
Description: Modus ponens inference with commutation of antecedents. (Contributed by NM, 17-Mar-1996.)
Hypotheses
Ref Expression
mpcom.1 (𝜓𝜑)
mpcom.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mpcom (𝜓𝜒)

Proof of Theorem mpcom
StepHypRef Expression
1 mpcom.1 . 2 (𝜓𝜑)
2 mpcom.2 . . 3 (𝜑 → (𝜓𝜒))
32com12 30 . 2 (𝜓 → (𝜑𝜒))
41, 3mpd 13 1 (𝜓𝜒)
Colors of variables: wff set 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:  syldan  280  ax16i  1830  ceqex  2807  sbcn1  2951  sbcim1  2952  sbcbi1  2953  sbcel21v  2968  peano2  4504  sotri  4929  relcoi1  5065  f0rn0  5312  f1ocnv  5373  tz6.12c  5444  funbrfv  5453  fnbrfvb  5455  fvmptss2  5489  elfvmptrab1  5508  oprabid  5796  eloprabga  5851  unielxp  6065  f1o2ndf1  6118  cnvoprab  6124  tfrlem1  6198  tfr1onlemaccex  6238  tfrcllemaccex  6251  ecopovtrn  6519  ecopovtrng  6522  findcard2d  6778  findcard2sd  6779  fidcenumlemr  6836  difinfsn  6978  ismkvnex  7022  ltexnqi  7210  prcdnql  7285  prcunqu  7286  prnmaxl  7289  prnminu  7290  ltprordil  7390  1idprl  7391  1idpru  7392  ltexprlemm  7401  ltexprlemopu  7404  ltexprlemru  7413  recexgt0sr  7574  mulgt0sr  7579  ltrenn  7656  nnindnn  7694  nnind  8729  nnmulcl  8734  nnnegz  9050  supinfneg  9383  infsupneg  9384  ublbneg  9398  ixxssxr  9676  ixxssixx  9678  iccshftri  9771  iccshftli  9773  iccdili  9775  icccntri  9777  1fv  9909  fzo1fzo0n0  9953  elfzonlteqm1  9980  ssfzo12  9994  exbtwnzlemshrink  10019  flqeqceilz  10084  zmodidfzoimp  10120  modfzo0difsn  10161  frec2uzltd  10169  frec2uzrdg  10175  frecuzrdgg  10182  seq3clss  10233  seq3fveq2  10235  seq3shft2  10239  monoord  10242  seq3split  10245  seq3caopr3  10247  seq3f1olemp  10268  seq3id2  10275  seq3homo  10276  seq3z  10277  ser3ge0  10283  exp3vallem  10287  fihashf1rn  10528  hashfzp1  10563  seq3coll  10578  cjre  10647  climeu  11058  climub  11106  fsum2d  11197  fsumabs  11227  fsumiun  11239  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  prodfap0  11307  prodfrecap  11308  ntrivcvgap  11310  dvdsabseq  11534  mulsucdiv2z  11571  nno  11592  nn0o  11593  dfgcd2  11691  lcmgcdlem  11747  cncongr2  11774  exprmfct  11807  ennnfoneleminc  11913  ennnfonelemkh  11914  ennnfonelemhf1o  11915  ennnfonelemhom  11917  setsn0fun  11985  tg2  12218  hmeof1o  12467  tgioo  12704  bdfind  13133  bj-nn0sucALT  13165  nninfsellemqall  13200
  Copyright terms: Public domain W3C validator