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-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syldan  280  ax16i  1838  ceqex  2839  sbcn1  2984  sbcim1  2985  sbcbi1  2986  sbcel21v  3001  peano2  4556  sotri  4983  relcoi1  5119  f0rn0  5366  f1ocnv  5429  tz6.12c  5500  funbrfv  5509  fnbrfvb  5511  fvmptss2  5545  elfvmptrab1  5564  oprabid  5855  eloprabga  5910  unielxp  6124  f1o2ndf1  6177  cnvoprab  6183  tfrlem1  6257  tfr1onlemaccex  6297  tfrcllemaccex  6310  ecopovtrn  6579  ecopovtrng  6582  findcard2d  6838  findcard2sd  6839  fidcenumlemr  6901  difinfsn  7046  nnnninfeq2  7074  ismkvnex  7100  cc3  7190  ltexnqi  7331  prcdnql  7406  prcunqu  7407  prnmaxl  7410  prnminu  7411  ltprordil  7511  1idprl  7512  1idpru  7513  ltexprlemm  7522  ltexprlemopu  7525  ltexprlemru  7534  recexgt0sr  7695  mulgt0sr  7700  ltrenn  7777  nnindnn  7815  nnind  8854  nnmulcl  8859  nnnegz  9175  supinfneg  9511  infsupneg  9512  ublbneg  9528  ixxssxr  9810  ixxssixx  9812  iccshftri  9905  iccshftli  9907  iccdili  9909  icccntri  9911  1fv  10047  fzo1fzo0n0  10091  elfzonlteqm1  10118  ssfzo12  10132  exbtwnzlemshrink  10157  flqeqceilz  10226  zmodidfzoimp  10262  modfzo0difsn  10303  frec2uzltd  10311  frec2uzrdg  10317  frecuzrdgg  10324  seq3clss  10375  seq3fveq2  10377  seq3shft2  10381  monoord  10384  seq3split  10387  seq3caopr3  10389  seq3f1olemp  10410  seq3id2  10417  seq3homo  10418  seq3z  10419  ser3ge0  10425  exp3vallem  10429  modqexp  10553  fihashf1rn  10674  hashfzp1  10709  seq3coll  10724  cjre  10793  climeu  11204  climub  11252  fsum2d  11343  fsumabs  11373  fsumiun  11385  cvgratnnlemnexp  11432  cvgratnnlemmn  11433  prodfap0  11453  prodfrecap  11454  ntrivcvgap  11456  fprodabs  11524  fprod2d  11531  dvdsmod0  11700  p1modz1  11701  dvdsmodexp  11702  dvdsabseq  11751  mulsucdiv2z  11788  nno  11809  nn0o  11810  dfgcd2  11913  lcmgcdlem  11969  cncongr2  11996  exprmfct  12030  eulerthlemrprm  12119  eulerthlema  12120  ennnfoneleminc  12210  ennnfonelemkh  12211  ennnfonelemhf1o  12212  ennnfonelemhom  12214  nninfdclemlt  12252  setsn0fun  12297  tg2  12530  hmeof1o  12779  tgioo  13016  bdfind  13592  bj-nn0sucALT  13624  nninfsellemqall  13658