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  1965  axc16i  2441  eupickbi  2637  ceqsalgALT  3467  cgsexg  3475  cgsex2g  3476  cgsex4g  3477  spcegv  3540  spc2egv  3542  disjne  4396  uneqdifeq  4433  preqsnd  4803  preq12nebg  4807  opthprneg  4809  dfiun2g  4973  axprlem4  5363  pocl  5540  relresfld  6234  unixpid  6242  ordnbtwn  6412  sucssel  6414  ordelinel  6420  funmo  6508  fvimacnv  6999  ordsuc  7758  tfi  7797  focdmex  7902  f1ovv  7904  opreuopreu  7980  frrlem4  8232  tz7.49  8377  oeworde  8522  fsetprcnex  8802  dom2d  8933  findcard  9091  fisupg  9191  dffi3  9337  noinfep  9572  cantnflem2  9602  ttrcltr  9628  tcmin  9651  rankr1ag  9717  rankunb  9765  rankxpsuc  9797  alephordi  9987  alephsucdom  9992  alephinit  10008  dfac9  10050  ackbij2lem4  10154  cff1  10171  cfslbn  10180  cfcoflem  10185  cfcof  10187  infpssrlem5  10220  isfin7-2  10309  acncc  10353  domtriomlem  10355  axdc3lem2  10364  ttukeylem1  10422  iundom2g  10453  axpowndlem3  10513  wunex2  10652  grupr  10711  gruiun  10713  eltskm  10757  nqereu  10843  addcanpr  10960  axpre-sup  11083  relin01  11665  nneo  12604  zeo2  12607  xrub  13255  uznfz  13555  difelfzle  13586  ssfzo12  13705  facndiv  14241  hashgt12el2  14376  hash2prde  14423  hash2pwpr  14429  hashle2prv  14431  tpfo  14453  fi1uzind  14460  swrdswrd  14658  pfxccatin12lem2  14684  pfxccatin12  14686  pfxccat3  14687  cshwidxmod  14756  2cshwcshw  14778  fsumcom2  15727  fprodss  15904  fprodcom2  15940  sumodd  16348  ndvdssub  16369  eucalglt  16545  prmind2  16645  coprm  16672  prmdiveq  16747  prmdvdsprmop  17005  prmgaplem5  17017  cicsym  17762  drsdir  18259  lublecllem  18315  istos  18373  tsrlin  18542  dirge  18560  mhmlin  18752  issubg2  19108  nsgbi  19123  symgextf1lem  19386  sylow2a  19585  gsumpr  19921  0ringnnzr  20493  0ring01eq  20497  01eq0ringOLD  20499  nrhmzr  20505  issubrng2  20526  issubrg2  20560  abvmul  20789  abvtri  20790  lmodlema  20851  rmodislmodlem  20915  rmodislmod  20916  ellspsn6  20980  lmhmlin  21022  lbsind  21067  nzerooringczr  21470  ipcj  21624  obsip  21711  lindsss  21814  mamufacex  22371  mavmulsolcl  22526  slesolvec  22654  inopn  22874  basis1  22925  tgss  22943  tgcl  22944  elcls3  23058  neindisj2  23098  cncls  23249  1stcelcls  23436  qtoptop2  23674  nrmr0reg  23724  fbasssin  23811  fbfinnfr  23816  fbunfip  23844  filufint  23895  uffix  23896  ufinffr  23904  ufilen  23905  fmfnfmlem1  23929  flftg  23971  alexsubALT  24026  xmeteq0  24313  blssexps  24401  blssex  24402  mopni3  24469  neibl  24476  metss  24483  metcnp3  24515  nmvs  24651  iccntr  24797  reconnlem2  24803  lebnumlem3  24940  caubl  25285  bcthlem5  25305  ovolunlem1  25474  voliunlem1  25527  volsuplem  25532  ellimc3  25856  logbgcd1irr  26771  lgsqrmodndvds  27330  gausslemma2dlem0i  27341  2lgsoddprmlem3  27391  dchrisumlema  27465  nofv  27635  nolesgn2o  27649  nogesgn1o  27651  nosupbnd1lem5  27690  addsprop  27982  negsprop  28041  mulsprop  28136  precsexlem6  28218  precsexlem7  28219  umgrnloopv  29189  usgrnloopvALT  29284  umgrres1lem  29393  upgrres1  29396  nbuhgr  29426  cplgrop  29520  fusgrregdegfi  29653  g0wlk0  29734  wlkdlem2  29765  upgrwlkdvdelem  29819  crctcshwlkn0lem3  29895  crctcshwlkn0lem5  29897  wspn0  30007  usgrwwlks2on  30041  umgrwwlks2on  30042  elwspths2spth  30053  clwlkclwwlklem2a  30083  clwlkclwwlklem3  30086  clwwlkn1loopb  30128  clwwlknonwwlknonb  30191  clwwlknonex2lem2  30193  3cyclfrgrrn2  30372  frgrncvvdeqlem8  30391  frgrwopregasn  30401  frgrwopregbsn  30402  frgrwopreg1  30403  frgrwopreg2  30404  frgrregord013  30480  frgrogt3nreg  30482  ablocom  30634  ubthlem1  30956  shaddcl  31303  shmulcl  31304  spansnss2  31661  cnopc  31999  cnfnc  32016  adj1  32019  pjorthcoi  32255  stj  32321  mdsl1i  32407  chirredlem1  32476  mdsymlem5  32493  cdj3lem2b  32523  slmdlema  33279  isprmidlc  33522  pconncn  35422  cvmlift2lem1  35500  fmla0xp  35581  ss2mcls  35766  antnestlaw2  35890  dfon2lem6  35984  waj-ax  36612  lukshef-ax2  36613  tr0elw  36682  bj-alrim  37006  bj-nexdt  37010  sucneqond  37695  rdgssun  37708  ptrecube  37955  poimirlem26  37981  poimirlem29  37984  heiborlem1  38146  rngodm1dm2  38267  rngoueqz  38275  zerdivemp1x  38282  isdrngo3  38294  0rngo  38362  pridl  38372  ispridlc  38405  isdmn3  38409  dmnnzd  38410  elrelscnveq3  38962  lshpcmp  39448  omllaw  39703  dochexmidlem7  41926  lspindp5  42230  zdivgd  42783  fsuppind  43037  dfac21  43512  eexinst11  44972  ax6e2eq  45002  e222  45081  e111  45119  e333  45177  natlocalincr  47322  imarnf1pr  47742  2ffzoeq  47788  iccpartigtl  47895  iccpartgt  47899  lighneallem3  48082  lighneal  48086  requad1  48110  evenltle  48205  fppr2odd  48219  sgoldbeven3prm  48271  bgoldbtbndlem2  48294  isubgr3stgrlem4  48457  isubgr3stgrlem7  48460  gpgedg2iv  48555  lincdifsn  48912  lindslinindimp2lem4  48949  snlindsntor  48959  lincresunit3lem1  48967  lincresunit3lem2  48968  f002  49341  setrec1lem2  50175