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

Step	Hyp	Ref	Expression
1		mpcom.1	. 2 ⊢ (𝜓 → 𝜑)
2		mpcom.2	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	com12 30	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
4	1, 3	mpd 13	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  syldan  277  ax16i  1787  ceqex  2745  sbcn1  2887  sbcim1  2888  sbcbi1  2889  sbcel21v  2904  peano2  4423  sotri  4840  relcoi1  4975  f0rn0  5218  f1ocnv  5279  tz6.12c  5347  funbrfv  5356  fnbrfvb  5358  fvmptss2  5392  oprabid  5695  eloprabga  5749  unielxp  5958  f1o2ndf1  6007  cnvoprab  6013  tfrlem1  6087  tfr1onlemaccex  6127  tfrcllemaccex  6140  ecopovtrn  6403  ecopovtrng  6406  findcard2d  6661  findcard2sd  6662  fidcenumlemr  6718  ltexnqi  7029  prcdnql  7104  prcunqu  7105  prnmaxl  7108  prnminu  7109  ltprordil  7209  1idprl  7210  1idpru  7211  ltexprlemm  7220  ltexprlemopu  7223  ltexprlemru  7232  recexgt0sr  7380  mulgt0sr  7384  ltrenn  7453  nnindnn  7489  nnind  8499  nnmulcl  8504  nnnegz  8814  supinfneg  9144  infsupneg  9145  ublbneg  9159  ixxssxr  9379  ixxssixx  9381  iccshftri  9473  iccshftli  9475  iccdili  9477  icccntri  9479  1fv  9611  fzo1fzo0n0  9655  elfzonlteqm1  9682  ssfzo12  9696  exbtwnzlemshrink  9721  flqeqceilz  9786  zmodidfzoimp  9822  modfzo0difsn  9863  frec2uzltd  9871  frec2uzrdg  9877  frecuzrdgg  9884  seq3clss  9948  iseqfveq2  9951  seq3fveq2  9953  iseqshft2  9959  monoord  9965  seq3split  9968  iseqsplit  9969  iseqcaopr3  9971  seq3f1olemp  9992  seq3id2  10001  iseqid2  10002  iseqhomo  10003  iseqz  10004  seq3homo  10005  ser3ge0  10013  exp3vallem  10017  fihashf1rn  10258  hashfzp1  10293  iseqcoll  10308  cjre  10377  climeu  10745  climub  10794  fsum2d  10890  fsumabs  10920  fsumiun  10932  cvgratnnlemnexp  10979  cvgratnnlemmn  10980  dvdsabseq  11187  mulsucdiv2z  11224  nno  11245  nn0o  11246  dfgcd2  11342  lcmgcdlem  11398  cncongr2  11425  exprmfct  11458  setsn0fun  11592  tg2  11821  bdfind  12114  bj-nn0sucALT  12146  nninfsellemqall  12179