Theorem syl5com 30

Description: Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.)

Hypotheses

Ref	Expression
syl5com.1	|- ( ph -> ps )
syl5com.2	|- ( ch -> ( ps -> th ) )

Assertion

Ref	Expression
syl5com	|- ( ph -> ( ch -> th ) )

Proof of Theorem syl5com

Step	Hyp	Ref	Expression
1		syl5com.1	. . 3 |- ( ph -> ps )
2	1	a1d 25	. 2 |- ( ph -> ( ch -> ps ) )
3		syl5com.2	. 2 |- ( ch -> ( ps -> th ) )
4	2, 3	sylcom 29	1 |- ( ph -> ( ch -> th ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  com12  31  syl5  32  axc11nlem  2001  axc11n  2002  axc16i  2017  mo2v  2264  mo2vOLD  2265  eupickbi  2349  ceqsalg  2995  cgsexg  3002  cgsex2g  3003  cgsex4g  3004  spc2egv  3056  spc3egv  3058  disjne  3721  uneqdifeq  3764  triun  4395  ordelord  4737  sucssel  4807  relresfld  5361  relcoi1  5363  unixpid  5369  fvimacnv  5815  ordsuc  6424  tfi  6463  fornex  6545  f1dmex  6546  f1ovv  6547  tz7.49  6896  oeworde  7028  undifixp  7295  dom2d  7346  2pwuninel  7462  findcard  7547  fisupg  7556  dffi3  7677  noinfep  7861  cantnflem2  7894  tcmin  7957  rankr1ag  8005  rankpwi  8026  rankelb  8027  rankunb  8053  rankxpsuc  8085  alephordi  8240  alephsucdom  8245  alephinit  8261  dfac9  8301  ackbij2lem4  8407  cff1  8423  cfslbn  8432  cfcoflem  8437  cfcof  8439  infpssrlem5  8472  isfin7-2  8561  acncc  8605  domtriomlem  8607  axdc3lem2  8616  ttukeylem1  8674  iundom2g  8700  axpowndlem3  8760  wunex2  8901  grupr  8960  gruiun  8962  eltskm  9006  nqereu  9094  addcanpr  9211  axpre-sup  9332  relin01  9860  nneo  10721  zeo2  10724  xrub  11270  uznfz  11539  ssfzo12  11616  facndiv  12060  hashf1rn  12119  hashgt12el2  12170  hash2prde  12175  hash2prd  12177  hash2pwpr  12178  brfi1uzind  12215  swrdswrd  12350  swrdccatin2  12374  swrdccatin12lem2  12376  swrdccatin12  12378  swrdccat3  12379  swrdccatid  12384  repswswrd  12418  fsumcom2  13237  incexclem  13295  isumrpcl  13302  ndvdssub  13607  eucalglt  13756  prmind2  13770  coprm  13782  prmdiveq  13857  drsdir  15101  lublecllem  15154  istos  15201  tsrlin  15385  dirge  15403  mhmlin  15467  issubg2  15689  nsgbi  15705  symgextf1lem  15918  sylow2a  16111  issubrg2  16865  abvmul  16894  abvtri  16895  lmodlema  16933  lspsnel6  17053  lmhmlin  17094  lbsind  17139  cygth  17963  ipcj  18022  obsip  18105  lindsss  18212  mamufacex  18248  mavmulsolcl  18321  slesolvec  18444  inopn  18471  basis1  18514  tgss  18532  tgcl  18533  elcls3  18646  neindisj2  18686  cnpco  18830  cncls  18837  1stcelcls  19024  txkgen  19184  qtoptop2  19231  nrmr0reg  19281  fbasssin  19368  fbfinnfr  19373  fbunfip  19401  filufint  19452  uffix  19453  ufinffr  19461  ufilen  19462  fmfnfmlem1  19486  flftg  19528  alexsubALT  19582  xmeteq0  19872  blssexps  19960  blssex  19961  mopni3  20028  neibl  20035  metss  20042  metcnp3  20074  nmvs  20216  reperflem  20354  iccntr  20357  reconnlem2  20363  lebnumlem3  20494  caubl  20777  bcthlem5  20798  ovolunlem1  20939  voliunlem1  20990  volsuplem  20995  ellimc3  21313  lhop1lem  21444  ulmss  21821  dchrisumlema  22696  usgrarnedg  23238  usgrafisbase  23262  sizeusglecusglem1  23327  uvtxisvtx  23333  usgrnloop  23397  usgrcyclnl2  23462  eupatrl  23524  ablocom  23707  rngodm1dm2  23840  rngoueqz  23852  zerdivemp1  23856  rngoridfz  23857  ubthlem1  24206  shaddcl  24554  shmulcl  24555  shmulclOLD  24556  spansnss2  24913  cnopc  25252  cnfnc  25269  adj1  25272  pjorthcoi  25508  stj  25574  mdsl1i  25660  chirredlem1  25729  mdsymlem5  25746  cdj3lem2b  25776  slmdlema  26152  pconcn  27043  cvmlift2lem1  27121  fprodss  27390  fprodcom2  27424  dfon2lem6  27530  wfrlem4  27656  wfrlem10  27662  frrlem4  27700  nofv  27727  nodenselem4  27754  waj-ax  28190  lukshef-ax2  28191  ontgval  28207  nn0prpw  28443  heiborlem1  28635  zerdivemp1x  28686  isdrngo3  28690  0rngo  28752  pridl  28762  ispridlc  28795  isdmn3  28799  dmnnzd  28800  dfac21  29344  2f1fvneq  30068  imarnf1pr  30075  2ffzoeq  30139  exprelprel  30154  wlkn0  30204  wlk0  30217  usgra2wlkspthlem1  30221  clwwlknprop  30360  clwlkisclwwlklem0  30375  wwlkext2clwwlk  30390  difelfzle  30412  cshwlemma1  30414  clwlkfclwwlk  30442  usgfiregdegfi  30453  usgrauvtxvd  30455  2pthfrgra  30528  3cyclfrgrarn2  30531  frgrancvvdeqlemB  30556  frgrawopreg1  30568  frgrawopreg2  30569  frgraeu  30572  numclwwlkovf2ex  30604  frgraregord013  30636  frgraogt3nreg  30638  gsumpr  30675  0rng01eq  30693  01eq0rng  30694  lincdifsn  30799  snlindsntor  30846  lincresunit3lem1  30854  lincresunit3lem2  30855  lincresunit3  30856  eexinst11  31065  ax6e2eq  31099  e222  31192  e111  31230  eel12131  31276  e333  31300  bj-axc11nlemv  32013  bj-axc11nv  32014  lshpcmp  32355  omllaw  32610  dochexmidlem7  34833  lspindp5  35137