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  speimfw  1743  axc11nlem  1946  axc11nlemOLD  2054  axc11n  2055  axc11nOLD  2056  axc16i  2070  mo2vOLD  2226  mo2vOLDOLD  2227  eupickbi  2292  2moOLD  2305  ceqsalgALT  3060  cgsexg  3067  cgsex2g  3068  cgsex4g  3069  spc2egv  3121  spc3egv  3123  disjne  3788  uneqdifeq  3832  triun  4473  sucssel  4884  relresfld  5442  relcoi1OLD  5445  unixpid  5451  fvimacnv  5904  ordsuc  6548  tfi  6587  fornex  6668  f1ovv  6670  tz7.49  7028  oeworde  7160  undifixp  7424  dom2d  7475  findcard  7674  fisupg  7683  dffi3  7806  noinfep  7990  cantnflem2  8022  tcmin  8085  rankr1ag  8133  rankpwi  8154  rankelb  8155  rankunb  8181  rankxpsuc  8213  alephordi  8368  alephsucdom  8373  alephinit  8389  dfac9  8429  ackbij2lem4  8535  cff1  8551  cfslbn  8560  cfcoflem  8565  cfcof  8567  infpssrlem5  8600  isfin7-2  8689  acncc  8733  domtriomlem  8735  axdc3lem2  8744  ttukeylem1  8802  iundom2g  8828  axpowndlem3  8887  wunex2  9027  grupr  9086  gruiun  9088  eltskm  9132  nqereu  9218  addcanpr  9335  axpre-sup  9457  relin01  9994  nneo  10863  zeo2  10866  xrub  11424  uznfz  11683  difelfzle  11710  ssfzo12  11804  facndiv  12268  hashf1rn  12327  hashgt12el2  12386  hash2prde  12420  hash2prd  12422  hash2pwpr  12423  exprelprel  12432  brfi1uzind  12436  swrdswrd  12596  swrdccatin2  12623  swrdccatin12lem2  12625  swrdccatin12  12627  swrdccat3  12628  swrdccatid  12633  repswswrd  12667  2cshwcshw  12704  relexpcnvd  12871  relexpdmd  12879  relexprnd  12883  relexpfldd  12885  relexpaddd  12889  fsumcom2  13591  incexclem  13650  fprodss  13757  fprodcom2  13790  ndvdssub  14067  eucalglt  14216  prmind2  14230  coprm  14243  prmdiveq  14318  drsdir  15681  lublecllem  15735  istos  15782  tsrlin  15966  dirge  15984  mhmlin  16090  issubg2  16333  nsgbi  16349  symgextf1lem  16562  sylow2a  16756  issubrg2  17562  abvmul  17591  abvtri  17592  lmodlema  17630  lspsnel6  17753  lmhmlin  17794  lbsind  17839  0ring01eq  18032  01eq0ring  18033  gsummoncoe1  18459  cygth  18701  ipcj  18760  obsip  18843  lindsss  18944  mamufacex  18976  mavmulsolcl  19138  slesolvec  19266  inopn  19493  basis1  19536  tgss  19555  tgcl  19556  elcls3  19670  neindisj2  19710  cnpco  19854  cncls  19861  1stcelcls  20047  txkgen  20238  qtoptop2  20285  nrmr0reg  20335  fbasssin  20422  fbfinnfr  20427  fbunfip  20455  filufint  20506  uffix  20507  ufinffr  20515  ufilen  20516  fmfnfmlem1  20540  flftg  20582  alexsubALT  20636  xmeteq0  20926  blssexps  21014  blssex  21015  mopni3  21082  neibl  21089  metss  21096  metcnp3  21128  nmvs  21270  reperflem  21408  iccntr  21411  reconnlem2  21417  lebnumlem3  21548  caubl  21831  bcthlem5  21852  ovolunlem1  21993  voliunlem1  22045  volsuplem  22050  ellimc3  22368  lhop1lem  22499  ulmss  22877  dchrisumlema  23790  usgrarnedg  24505  usgrafisbase  24535  sizeusglecusglem1  24605  uvtxisvtx  24611  wlkn0  24648  usgrnloop  24686  usgra2wlkspthlem1  24740  usgrcyclnl2  24762  wlk0  24882  clwwlknprop  24893  clwlkisclwwlklem0  24909  wwlkext2clwwlk  24924  clwlkfclwwlk  24965  usgfiregdegfi  25032  eupatrl  25089  2pthfrgra  25132  3cyclfrgrarn2  25135  frgrancvvdeqlemB  25159  frgrawopreg1  25171  frgrawopreg2  25172  frgraeu  25175  numclwwlkovf2ex  25207  frgraregord013  25239  frgraogt3nreg  25241  ablocom  25404  rngodm1dm2  25537  rngoueqz  25549  zerdivemp1  25553  rngoridfz  25554  ubthlem1  25903  shaddcl  26251  shmulcl  26252  shmulclOLD  26253  spansnss2  26610  cnopc  26948  cnfnc  26965  adj1  26968  pjorthcoi  27204  stj  27270  mdsl1i  27356  chirredlem1  27425  mdsymlem5  27442  cdj3lem2b  27472  slmdlema  27899  pconcn  28858  cvmlift2lem1  28936  ss2mcls  29117  dfon2lem6  29385  wfrlem4  29511  wfrlem10  29517  frrlem4  29555  nofv  29582  nodenselem4  29609  waj-ax  30032  lukshef-ax2  30033  ontgval  30049  nn0prpw  30307  heiborlem1  30473  zerdivemp1x  30524  isdrngo3  30528  0rngo  30590  pridl  30600  ispridlc  30633  isdmn3  30637  dmnnzd  30638  dfac21  31178  pfxccatin12lem2  32599  pfxccatin12  32600  pfxccat3  32601  2f1fvneq  32628  imarnf1pr  32630  2ffzoeq  32661  usgrauvtxvd  32676  usgo0s0  32753  usgo0s0ALT  32754  usgo1s0ALT  32755  usgo1s0  32760  usgresvm1  32761  usgresvm1ALT  32765  nrhmzr  32879  nzerooringczr  33080  gsumpr  33150  lincdifsn  33225  snlindsntor  33272  lincresunit3lem1  33280  lincresunit3lem2  33281  lincresunit3  33282  eexinst11  33630  ax6e2eq  33670  e222  33762  e111  33800  eel12131  33846  e333  33870  bj-alrim  34593  bj-nexdt  34597  bj-axc11nlemv  34662  bj-axc11nv  34663  lshpcmp  35126  omllaw  35381  dochexmidlem7  37606  lspindp5  37910