Theorem syl5com 31

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 26	. 2 |- ( ph -> ( ch -> ps ) )
3		syl5com.2	. 2 |- ( ch -> ( ps -> th ) )
4	2, 3	sylcom 30	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  32  syl5  33  speimfw  1785  axc11nlem  1996  axc11nlemOLD  2104  axc11n  2105  axc11nOLD  2106  axc16i  2120  mo2vOLD  2274  mo2vOLDOLD  2275  eupickbi  2339  2moOLD  2352  ceqsalgALT  3113  cgsexg  3120  cgsex2g  3121  cgsex4g  3122  spc2egv  3174  spc3egv  3176  disjne  3844  uneqdifeq  3890  triun  4533  relresfld  5382  relcoi1OLD  5385  unixpid  5391  sucssel  5534  fvimacnv  6012  ordsuc  6655  tfi  6694  fornex  6776  f1ovv  6778  wfrlem4  7047  wfrlem10  7053  tz7.49  7170  oeworde  7302  undifixp  7566  dom2d  7617  findcard  7816  fisupg  7825  dffi3  7951  noinfep  8164  cantnflem2  8194  tcmin  8224  rankr1ag  8272  rankpwi  8293  rankelb  8294  rankunb  8320  rankxpsuc  8352  alephordi  8503  alephsucdom  8508  alephinit  8524  dfac9  8564  ackbij2lem4  8670  cff1  8686  cfslbn  8695  cfcoflem  8700  cfcof  8702  infpssrlem5  8735  isfin7-2  8824  acncc  8868  domtriomlem  8870  axdc3lem2  8879  ttukeylem1  8937  iundom2g  8963  axpowndlem3  9022  wunex2  9162  grupr  9221  gruiun  9223  eltskm  9267  nqereu  9353  addcanpr  9470  axpre-sup  9592  relin01  10137  nneo  11019  zeo2  11022  xrub  11597  uznfz  11875  difelfzle  11902  ssfzo12  12001  facndiv  12470  hashf1rn  12532  hashgt12el2  12591  hash2prde  12625  hash2prd  12627  hash2pwpr  12628  exprelprel  12637  brfi1uzind  12641  swrdswrd  12801  swrdccatin2  12828  swrdccatin12lem2  12830  swrdccatin12  12832  swrdccat3  12833  swrdccatid  12838  repswswrd  12872  2cshwcshw  12909  relexpcnvd  13078  relexpdmd  13086  relexprnd  13090  relexpfldd  13092  relexpaddd  13096  fsumcom2  13813  incexclem  13872  fprodss  13980  fprodcom2  14016  ndvdssub  14363  eucalglt  14515  prmind2  14606  coprm  14628  prmdiveq  14703  prmdvdsprmop  14964  prmdvdsprmorpOLD  14979  prmgaplem5  14988  drsdir  16131  lublecllem  16185  istos  16232  tsrlin  16416  dirge  16434  mhmlin  16540  issubg2  16783  nsgbi  16799  symgextf1lem  17012  sylow2a  17206  issubrg2  17963  abvmul  17992  abvtri  17993  lmodlema  18031  lspsnel6  18152  lmhmlin  18193  lbsind  18238  0ring01eq  18430  01eq0ring  18431  gsummoncoe1  18833  cygth  19073  ipcj  19132  obsip  19215  lindsss  19313  mamufacex  19345  mavmulsolcl  19507  slesolvec  19635  inopn  19860  basis1  19896  tgss  19915  tgcl  19916  elcls3  20030  neindisj2  20070  cnpco  20214  cncls  20221  1stcelcls  20407  txkgen  20598  qtoptop2  20645  nrmr0reg  20695  fbasssin  20782  fbfinnfr  20787  fbunfip  20815  filufint  20866  uffix  20867  ufinffr  20875  ufilen  20876  fmfnfmlem1  20900  flftg  20942  alexsubALT  20997  xmeteq0  21284  blssexps  21372  blssex  21373  mopni3  21440  neibl  21447  metss  21454  metcnp3  21486  nmvs  21610  reperflem  21747  iccntr  21750  reconnlem2  21756  lebnumlem3  21887  caubl  22170  bcthlem5  22189  ovolunlem1  22328  voliunlem1  22380  volsuplem  22385  ellimc3  22711  lhop1lem  22842  ulmss  23217  dchrisumlema  24189  usgrarnedg  24957  usgrafisbase  24987  sizeusglecusglem1  25057  uvtxisvtx  25063  wlkn0  25100  usgrnloop  25138  usgra2wlkspthlem1  25192  usgrcyclnl2  25214  wlk0  25334  clwwlknprop  25345  clwlkisclwwlklem0  25361  wwlkext2clwwlk  25376  clwlkfclwwlk  25417  usgfiregdegfi  25484  eupatrl  25541  2pthfrgra  25584  3cyclfrgrarn2  25587  frgrancvvdeqlemB  25611  frgrawopreg1  25623  frgrawopreg2  25624  frgraeu  25627  numclwwlkovf2ex  25659  frgraregord013  25691  frgraogt3nreg  25693  ablocom  25858  rngodm1dm2  25991  rngoueqz  26003  zerdivemp1  26007  rngoridfz  26008  ubthlem1  26357  shaddcl  26705  shmulcl  26706  spansnss2  27063  cnopc  27401  cnfnc  27418  adj1  27421  pjorthcoi  27657  stj  27723  mdsl1i  27809  chirredlem1  27878  mdsymlem5  27895  cdj3lem2b  27925  slmdlema  28357  pconcn  29735  cvmlift2lem1  29813  ss2mcls  29994  dfon2lem6  30221  frrlem4  30304  nofv  30331  nodenselem4  30358  nn0prpw  30764  waj-ax  30859  lukshef-ax2  30860  ontgval  30876  bj-alrim  31026  bj-nexdt  31030  bj-axc11nlemv  31095  bj-axc11nv  31096  ptrecube  31643  poimirlem26  31669  poimirlem29  31672  heiborlem1  31846  zerdivemp1x  31897  isdrngo3  31901  0rngo  31963  pridl  31973  ispridlc  32006  isdmn3  32010  dmnnzd  32011  lshpcmp  32262  omllaw  32517  dochexmidlem7  34742  lspindp5  35046  dfac21  35629  eexinst11  36520  ax6e2eq  36560  e222  36652  e111  36690  eel12131  36736  e333  36759  iccpartigtl  38126  iccpartgt  38130  bgoldbtbndlem2  38290  bgoldbtbndlem3  38291  pfxccatin12lem2  38354  pfxccatin12  38355  pfxccat3  38356  2f1fvneq  38383  imarnf1pr  38385  2ffzoeq  38412  usgrauvtxvd  38427  usgo0s0  38504  usgo0s0ALT  38505  usgo1s0ALT  38506  usgo1s0  38511  usgresvm1  38512  usgresvm1ALT  38516  nrhmzr  38630  nzerooringczr  38831  gsumpr  38901  lincdifsn  38976  snlindsntor  39023  lincresunit3lem1  39031  lincresunit3lem2  39032  lincresunit3  39033