Theorem syl5com 31

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

Hypotheses

Ref	Expression
syl5com.1	⊢ (𝜑 → 𝜓)
syl5com.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
syl5com	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem syl5com

Step	Hyp	Ref	Expression
1		syl5com.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
3		syl5com.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	sylcom 30	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:  com12  32  syl5  34  speimfw  1963  axc16i  2434  eupickbi  2629  ceqsalgALT  3484  cgsexg  3492  cgsex2g  3493  cgsex4g  3494  cgsex4gOLD  3495  spcegv  3563  spc2egv  3565  disjne  4418  uneqdifeq  4456  preqsnd  4823  preq12nebg  4827  opthprneg  4829  dfiun2g  4994  axprlem4  5381  pocl  5554  relresfld  6249  unixpid  6257  ordnbtwn  6427  sucssel  6429  ordelinel  6435  funmo  6531  fvimacnv  7025  ordsuc  7788  ordsucOLD  7789  tfi  7829  focdmex  7934  f1ovv  7936  opreuopreu  8013  frrlem4  8268  tz7.49  8413  oeworde  8557  fsetprcnex  8835  dom2d  8964  findcard  9127  fisupg  9235  dffi3  9382  noinfep  9613  cantnflem2  9643  ttrcltr  9669  tcmin  9694  rankr1ag  9755  rankunb  9803  rankxpsuc  9835  alephordi  10027  alephsucdom  10032  alephinit  10048  dfac9  10090  ackbij2lem4  10194  cff1  10211  cfslbn  10220  cfcoflem  10225  cfcof  10227  infpssrlem5  10260  isfin7-2  10349  acncc  10393  domtriomlem  10395  axdc3lem2  10404  ttukeylem1  10462  iundom2g  10493  axpowndlem3  10552  wunex2  10691  grupr  10750  gruiun  10752  eltskm  10796  nqereu  10882  addcanpr  10999  axpre-sup  11122  relin01  11702  nneo  12618  zeo2  12621  xrub  13272  uznfz  13571  difelfzle  13602  ssfzo12  13720  facndiv  14253  hashgt12el2  14388  hash2prde  14435  hash2pwpr  14441  hashle2prv  14443  tpfo  14465  fi1uzind  14472  swrdswrd  14670  pfxccatin12lem2  14696  pfxccatin12  14698  pfxccat3  14699  cshwidxmod  14768  2cshwcshw  14791  fsumcom2  15740  fprodss  15914  fprodcom2  15950  sumodd  16358  ndvdssub  16379  eucalglt  16555  prmind2  16655  coprm  16681  prmdiveq  16756  prmdvdsprmop  17014  prmgaplem5  17026  cicsym  17766  drsdir  18263  lublecllem  18319  istos  18377  tsrlin  18544  dirge  18562  mhmlin  18720  issubg2  19073  nsgbi  19089  symgextf1lem  19350  sylow2a  19549  gsumpr  19885  0ringnnzr  20434  0ring01eq  20438  01eq0ringOLD  20440  nrhmzr  20446  issubrng2  20467  issubrg2  20501  abvmul  20730  abvtri  20731  lmodlema  20771  rmodislmodlem  20835  rmodislmod  20836  ellspsn6  20900  lmhmlin  20942  lbsind  20987  nzerooringczr  21390  ipcj  21543  obsip  21630  lindsss  21733  mamufacex  22283  mavmulsolcl  22438  slesolvec  22566  inopn  22786  basis1  22837  tgss  22855  tgcl  22856  elcls3  22970  neindisj2  23010  cncls  23161  1stcelcls  23348  qtoptop2  23586  nrmr0reg  23636  fbasssin  23723  fbfinnfr  23728  fbunfip  23756  filufint  23807  uffix  23808  ufinffr  23816  ufilen  23817  fmfnfmlem1  23841  flftg  23883  alexsubALT  23938  xmeteq0  24226  blssexps  24314  blssex  24315  mopni3  24382  neibl  24389  metss  24396  metcnp3  24428  nmvs  24564  iccntr  24710  reconnlem2  24716  lebnumlem3  24862  caubl  25208  bcthlem5  25228  ovolunlem1  25398  voliunlem1  25451  volsuplem  25456  ellimc3  25780  logbgcd1irr  26704  lgsqrmodndvds  27264  gausslemma2dlem0i  27275  2lgsoddprmlem3  27325  dchrisumlema  27399  nofv  27569  nolesgn2o  27583  nogesgn1o  27585  nosupbnd1lem5  27624  addsprop  27883  negsprop  27941  mulsprop  28033  precsexlem6  28114  precsexlem7  28115  umgrnloopv  29033  usgrnloopvALT  29128  umgrres1lem  29237  upgrres1  29240  nbuhgr  29270  cplgrop  29364  fusgrregdegfi  29497  g0wlk0  29580  wlkdlem2  29611  upgrwlkdvdelem  29666  crctcshwlkn0lem3  29742  crctcshwlkn0lem5  29744  wspn0  29854  umgrwwlks2on  29887  elwspths2spth  29897  clwlkclwwlklem2a  29927  clwlkclwwlklem3  29930  clwwlkn1loopb  29972  clwwlknonwwlknonb  30035  clwwlknonex2lem2  30037  3cyclfrgrrn2  30216  frgrncvvdeqlem8  30235  frgrwopregasn  30245  frgrwopregbsn  30246  frgrwopreg1  30247  frgrwopreg2  30248  frgrregord013  30324  frgrogt3nreg  30326  ablocom  30477  ubthlem1  30799  shaddcl  31146  shmulcl  31147  spansnss2  31504  cnopc  31842  cnfnc  31859  adj1  31862  pjorthcoi  32098  stj  32164  mdsl1i  32250  chirredlem1  32319  mdsymlem5  32336  cdj3lem2b  32366  slmdlema  33156  isprmidlc  33418  pconncn  35211  cvmlift2lem1  35289  fmla0xp  35370  ss2mcls  35555  antnestlaw2  35679  dfon2lem6  35776  waj-ax  36402  lukshef-ax2  36403  bj-alrim  36681  bj-nexdt  36685  sucneqond  37353  rdgssun  37366  ptrecube  37614  poimirlem26  37640  poimirlem29  37643  heiborlem1  37805  rngodm1dm2  37926  rngoueqz  37934  zerdivemp1x  37941  isdrngo3  37953  0rngo  38021  pridl  38031  ispridlc  38064  isdmn3  38068  dmnnzd  38069  elrelscnveq3  38482  lshpcmp  38981  omllaw  39236  dochexmidlem7  41460  lspindp5  41764  zdivgd  42325  fsuppind  42578  dfac21  43055  eexinst11  44517  ax6e2eq  44547  e222  44626  e111  44664  e333  44722  natlocalincr  46874  tworepnotupword  46884  imarnf1pr  47283  2ffzoeq  47328  iccpartigtl  47424  iccpartgt  47428  lighneallem3  47608  lighneal  47612  requad1  47623  evenltle  47718  fppr2odd  47732  sgoldbeven3prm  47784  bgoldbtbndlem2  47807  isubgr3stgrlem4  47968  isubgr3stgrlem7  47971  gpgedg2iv  48058  lincdifsn  48413  lindslinindimp2lem4  48450  snlindsntor  48460  lincresunit3lem1  48468  lincresunit3lem2  48469  f002  48842  setrec1lem2  49677