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  3479  cgsexg  3487  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  spcegv  3553  spc2egv  3555  disjne  4409  uneqdifeq  4447  preqsnd  4817  preq12nebg  4821  opthprneg  4823  dfiun2g  4987  axprlem4  5373  pocl  5548  relresfld  6242  unixpid  6250  ordnbtwn  6420  sucssel  6422  ordelinel  6428  funmo  6516  fvimacnv  7007  ordsuc  7766  tfi  7805  focdmex  7910  f1ovv  7912  opreuopreu  7988  frrlem4  8241  tz7.49  8386  oeworde  8531  fsetprcnex  8811  dom2d  8942  findcard  9100  fisupg  9200  dffi3  9346  noinfep  9581  cantnflem2  9611  ttrcltr  9637  tcmin  9660  rankr1ag  9726  rankunb  9774  rankxpsuc  9806  alephordi  9996  alephsucdom  10001  alephinit  10017  dfac9  10059  ackbij2lem4  10163  cff1  10180  cfslbn  10189  cfcoflem  10194  cfcof  10196  infpssrlem5  10229  isfin7-2  10318  acncc  10362  domtriomlem  10364  axdc3lem2  10373  ttukeylem1  10431  iundom2g  10462  axpowndlem3  10522  wunex2  10661  grupr  10720  gruiun  10722  eltskm  10766  nqereu  10852  addcanpr  10969  axpre-sup  11092  relin01  11673  nneo  12588  zeo2  12591  xrub  13239  uznfz  13538  difelfzle  13569  ssfzo12  13687  facndiv  14223  hashgt12el2  14358  hash2prde  14405  hash2pwpr  14411  hashle2prv  14413  tpfo  14435  fi1uzind  14442  swrdswrd  14640  pfxccatin12lem2  14666  pfxccatin12  14668  pfxccat3  14669  cshwidxmod  14738  2cshwcshw  14760  fsumcom2  15709  fprodss  15883  fprodcom2  15919  sumodd  16327  ndvdssub  16348  eucalglt  16524  prmind2  16624  coprm  16650  prmdiveq  16725  prmdvdsprmop  16983  prmgaplem5  16995  cicsym  17740  drsdir  18237  lublecllem  18293  istos  18351  tsrlin  18520  dirge  18538  mhmlin  18730  issubg2  19083  nsgbi  19098  symgextf1lem  19361  sylow2a  19560  gsumpr  19896  0ringnnzr  20470  0ring01eq  20474  01eq0ringOLD  20476  nrhmzr  20482  issubrng2  20503  issubrg2  20537  abvmul  20766  abvtri  20767  lmodlema  20828  rmodislmodlem  20892  rmodislmod  20893  ellspsn6  20957  lmhmlin  20999  lbsind  21044  nzerooringczr  21447  ipcj  21601  obsip  21688  lindsss  21791  mamufacex  22352  mavmulsolcl  22507  slesolvec  22635  inopn  22855  basis1  22906  tgss  22924  tgcl  22925  elcls3  23039  neindisj2  23079  cncls  23230  1stcelcls  23417  qtoptop2  23655  nrmr0reg  23705  fbasssin  23792  fbfinnfr  23797  fbunfip  23825  filufint  23876  uffix  23877  ufinffr  23885  ufilen  23886  fmfnfmlem1  23910  flftg  23952  alexsubALT  24007  xmeteq0  24294  blssexps  24382  blssex  24383  mopni3  24450  neibl  24457  metss  24464  metcnp3  24496  nmvs  24632  iccntr  24778  reconnlem2  24784  lebnumlem3  24930  caubl  25276  bcthlem5  25296  ovolunlem1  25466  voliunlem1  25519  volsuplem  25524  ellimc3  25848  logbgcd1irr  26772  lgsqrmodndvds  27332  gausslemma2dlem0i  27343  2lgsoddprmlem3  27393  dchrisumlema  27467  nofv  27637  nolesgn2o  27651  nogesgn1o  27653  nosupbnd1lem5  27692  addsprop  27984  negsprop  28043  mulsprop  28138  precsexlem6  28220  precsexlem7  28221  umgrnloopv  29191  usgrnloopvALT  29286  umgrres1lem  29395  upgrres1  29398  nbuhgr  29428  cplgrop  29522  fusgrregdegfi  29655  g0wlk0  29736  wlkdlem2  29767  upgrwlkdvdelem  29821  crctcshwlkn0lem3  29897  crctcshwlkn0lem5  29899  wspn0  30009  usgrwwlks2on  30043  umgrwwlks2on  30044  elwspths2spth  30055  clwlkclwwlklem2a  30085  clwlkclwwlklem3  30088  clwwlkn1loopb  30130  clwwlknonwwlknonb  30193  clwwlknonex2lem2  30195  3cyclfrgrrn2  30374  frgrncvvdeqlem8  30393  frgrwopregasn  30403  frgrwopregbsn  30404  frgrwopreg1  30405  frgrwopreg2  30406  frgrregord013  30482  frgrogt3nreg  30484  ablocom  30635  ubthlem1  30957  shaddcl  31304  shmulcl  31305  spansnss2  31662  cnopc  32000  cnfnc  32017  adj1  32020  pjorthcoi  32256  stj  32322  mdsl1i  32408  chirredlem1  32477  mdsymlem5  32494  cdj3lem2b  32524  slmdlema  33296  isprmidlc  33539  pconncn  35437  cvmlift2lem1  35515  fmla0xp  35596  ss2mcls  35781  antnestlaw2  35905  dfon2lem6  35999  waj-ax  36627  lukshef-ax2  36628  bj-alrim  36932  bj-nexdt  36936  sucneqond  37614  rdgssun  37627  ptrecube  37865  poimirlem26  37891  poimirlem29  37894  heiborlem1  38056  rngodm1dm2  38177  rngoueqz  38185  zerdivemp1x  38192  isdrngo3  38204  0rngo  38272  pridl  38282  ispridlc  38315  isdmn3  38319  dmnnzd  38320  elrelscnveq3  38872  lshpcmp  39358  omllaw  39613  dochexmidlem7  41836  lspindp5  42140  zdivgd  42701  fsuppind  42942  dfac21  43417  eexinst11  44877  ax6e2eq  44907  e222  44986  e111  45024  e333  45082  natlocalincr  47228  imarnf1pr  47636  2ffzoeq  47681  iccpartigtl  47777  iccpartgt  47781  lighneallem3  47961  lighneal  47965  requad1  47976  evenltle  48071  fppr2odd  48085  sgoldbeven3prm  48137  bgoldbtbndlem2  48160  isubgr3stgrlem4  48323  isubgr3stgrlem7  48326  gpgedg2iv  48421  lincdifsn  48778  lindslinindimp2lem4  48815  snlindsntor  48825  lincresunit3lem1  48833  lincresunit3lem2  48834  f002  49207  setrec1lem2  50041