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  3475  cgsexg  3483  cgsex2g  3484  cgsex4g  3485  cgsex4gOLD  3486  spcegv  3554  spc2egv  3556  disjne  4408  uneqdifeq  4446  preqsnd  4813  preq12nebg  4817  opthprneg  4819  dfiun2g  4983  axprlem4  5368  pocl  5539  relresfld  6228  unixpid  6236  ordnbtwn  6406  sucssel  6408  ordelinel  6414  funmo  6502  fvimacnv  6991  ordsuc  7752  ordsucOLD  7753  tfi  7793  focdmex  7898  f1ovv  7900  opreuopreu  7976  frrlem4  8229  tz7.49  8374  oeworde  8518  fsetprcnex  8796  dom2d  8925  findcard  9087  fisupg  9193  dffi3  9340  noinfep  9575  cantnflem2  9605  ttrcltr  9631  tcmin  9656  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  10512  wunex2  10651  grupr  10710  gruiun  10712  eltskm  10756  nqereu  10842  addcanpr  10959  axpre-sup  11082  relin01  11662  nneo  12578  zeo2  12581  xrub  13232  uznfz  13531  difelfzle  13562  ssfzo12  13680  facndiv  14213  hashgt12el2  14348  hash2prde  14395  hash2pwpr  14401  hashle2prv  14403  tpfo  14425  fi1uzind  14432  swrdswrd  14629  pfxccatin12lem2  14655  pfxccatin12  14657  pfxccat3  14658  cshwidxmod  14727  2cshwcshw  14750  fsumcom2  15699  fprodss  15873  fprodcom2  15909  sumodd  16317  ndvdssub  16338  eucalglt  16514  prmind2  16614  coprm  16640  prmdiveq  16715  prmdvdsprmop  16973  prmgaplem5  16985  cicsym  17729  drsdir  18226  lublecllem  18282  istos  18340  tsrlin  18509  dirge  18527  mhmlin  18685  issubg2  19038  nsgbi  19054  symgextf1lem  19317  sylow2a  19516  gsumpr  19852  0ringnnzr  20428  0ring01eq  20432  01eq0ringOLD  20434  nrhmzr  20440  issubrng2  20461  issubrg2  20495  abvmul  20724  abvtri  20725  lmodlema  20786  rmodislmodlem  20850  rmodislmod  20851  ellspsn6  20915  lmhmlin  20957  lbsind  21002  nzerooringczr  21405  ipcj  21559  obsip  21646  lindsss  21749  mamufacex  22299  mavmulsolcl  22454  slesolvec  22582  inopn  22802  basis1  22853  tgss  22871  tgcl  22872  elcls3  22986  neindisj2  23026  cncls  23177  1stcelcls  23364  qtoptop2  23602  nrmr0reg  23652  fbasssin  23739  fbfinnfr  23744  fbunfip  23772  filufint  23823  uffix  23824  ufinffr  23832  ufilen  23833  fmfnfmlem1  23857  flftg  23899  alexsubALT  23954  xmeteq0  24242  blssexps  24330  blssex  24331  mopni3  24398  neibl  24405  metss  24412  metcnp3  24444  nmvs  24580  iccntr  24726  reconnlem2  24732  lebnumlem3  24878  caubl  25224  bcthlem5  25244  ovolunlem1  25414  voliunlem1  25467  volsuplem  25472  ellimc3  25796  logbgcd1irr  26720  lgsqrmodndvds  27280  gausslemma2dlem0i  27291  2lgsoddprmlem3  27341  dchrisumlema  27415  nofv  27585  nolesgn2o  27599  nogesgn1o  27601  nosupbnd1lem5  27640  addsprop  27906  negsprop  27964  mulsprop  28056  precsexlem6  28137  precsexlem7  28138  umgrnloopv  29069  usgrnloopvALT  29164  umgrres1lem  29273  upgrres1  29276  nbuhgr  29306  cplgrop  29400  fusgrregdegfi  29533  g0wlk0  29614  wlkdlem2  29645  upgrwlkdvdelem  29699  crctcshwlkn0lem3  29775  crctcshwlkn0lem5  29777  wspn0  29887  umgrwwlks2on  29920  elwspths2spth  29930  clwlkclwwlklem2a  29960  clwlkclwwlklem3  29963  clwwlkn1loopb  30005  clwwlknonwwlknonb  30068  clwwlknonex2lem2  30070  3cyclfrgrrn2  30249  frgrncvvdeqlem8  30268  frgrwopregasn  30278  frgrwopregbsn  30279  frgrwopreg1  30280  frgrwopreg2  30281  frgrregord013  30357  frgrogt3nreg  30359  ablocom  30510  ubthlem1  30832  shaddcl  31179  shmulcl  31180  spansnss2  31537  cnopc  31875  cnfnc  31892  adj1  31895  pjorthcoi  32131  stj  32197  mdsl1i  32283  chirredlem1  32352  mdsymlem5  32369  cdj3lem2b  32399  slmdlema  33158  isprmidlc  33397  pconncn  35199  cvmlift2lem1  35277  fmla0xp  35358  ss2mcls  35543  antnestlaw2  35667  dfon2lem6  35764  waj-ax  36390  lukshef-ax2  36391  bj-alrim  36669  bj-nexdt  36673  sucneqond  37341  rdgssun  37354  ptrecube  37602  poimirlem26  37628  poimirlem29  37631  heiborlem1  37793  rngodm1dm2  37914  rngoueqz  37922  zerdivemp1x  37929  isdrngo3  37941  0rngo  38009  pridl  38019  ispridlc  38052  isdmn3  38056  dmnnzd  38057  elrelscnveq3  38470  lshpcmp  38969  omllaw  39224  dochexmidlem7  41448  lspindp5  41752  zdivgd  42313  fsuppind  42566  dfac21  43042  eexinst11  44504  ax6e2eq  44534  e222  44613  e111  44651  e333  44709  natlocalincr  46861  tworepnotupword  46871  imarnf1pr  47270  2ffzoeq  47315  iccpartigtl  47411  iccpartgt  47415  lighneallem3  47595  lighneal  47599  requad1  47610  evenltle  47705  fppr2odd  47719  sgoldbeven3prm  47771  bgoldbtbndlem2  47794  isubgr3stgrlem4  47957  isubgr3stgrlem7  47960  gpgedg2iv  48055  lincdifsn  48413  lindslinindimp2lem4  48450  snlindsntor  48460  lincresunit3lem1  48468  lincresunit3lem2  48469  f002  48842  setrec1lem2  49677