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  2435  eupickbi  2630  ceqsalgALT  3487  cgsexg  3495  cgsex2g  3496  cgsex4g  3497  cgsex4gOLD  3498  spcegv  3566  spc2egv  3568  disjne  4421  uneqdifeq  4459  preqsnd  4826  preq12nebg  4830  opthprneg  4832  dfiun2g  4997  axprlem4  5384  pocl  5557  relresfld  6252  unixpid  6260  ordnbtwn  6430  sucssel  6432  ordelinel  6438  funmo  6534  fvimacnv  7028  ordsuc  7791  ordsucOLD  7792  tfi  7832  focdmex  7937  f1ovv  7939  opreuopreu  8016  frrlem4  8271  tz7.49  8416  oeworde  8560  fsetprcnex  8838  dom2d  8967  findcard  9133  fisupg  9242  dffi3  9389  noinfep  9620  cantnflem2  9650  ttrcltr  9676  tcmin  9701  rankr1ag  9762  rankunb  9810  rankxpsuc  9842  alephordi  10034  alephsucdom  10039  alephinit  10055  dfac9  10097  ackbij2lem4  10201  cff1  10218  cfslbn  10227  cfcoflem  10232  cfcof  10234  infpssrlem5  10267  isfin7-2  10356  acncc  10400  domtriomlem  10402  axdc3lem2  10411  ttukeylem1  10469  iundom2g  10500  axpowndlem3  10559  wunex2  10698  grupr  10757  gruiun  10759  eltskm  10803  nqereu  10889  addcanpr  11006  axpre-sup  11129  relin01  11709  nneo  12625  zeo2  12628  xrub  13279  uznfz  13578  difelfzle  13609  ssfzo12  13727  facndiv  14260  hashgt12el2  14395  hash2prde  14442  hash2pwpr  14448  hashle2prv  14450  tpfo  14472  fi1uzind  14479  swrdswrd  14677  pfxccatin12lem2  14703  pfxccatin12  14705  pfxccat3  14706  cshwidxmod  14775  2cshwcshw  14798  fsumcom2  15747  fprodss  15921  fprodcom2  15957  sumodd  16365  ndvdssub  16386  eucalglt  16562  prmind2  16662  coprm  16688  prmdiveq  16763  prmdvdsprmop  17021  prmgaplem5  17033  cicsym  17773  drsdir  18270  lublecllem  18326  istos  18384  tsrlin  18551  dirge  18569  mhmlin  18727  issubg2  19080  nsgbi  19096  symgextf1lem  19357  sylow2a  19556  gsumpr  19892  0ringnnzr  20441  0ring01eq  20445  01eq0ringOLD  20447  nrhmzr  20453  issubrng2  20474  issubrg2  20508  abvmul  20737  abvtri  20738  lmodlema  20778  rmodislmodlem  20842  rmodislmod  20843  ellspsn6  20907  lmhmlin  20949  lbsind  20994  nzerooringczr  21397  ipcj  21550  obsip  21637  lindsss  21740  mamufacex  22290  mavmulsolcl  22445  slesolvec  22573  inopn  22793  basis1  22844  tgss  22862  tgcl  22863  elcls3  22977  neindisj2  23017  cncls  23168  1stcelcls  23355  qtoptop2  23593  nrmr0reg  23643  fbasssin  23730  fbfinnfr  23735  fbunfip  23763  filufint  23814  uffix  23815  ufinffr  23823  ufilen  23824  fmfnfmlem1  23848  flftg  23890  alexsubALT  23945  xmeteq0  24233  blssexps  24321  blssex  24322  mopni3  24389  neibl  24396  metss  24403  metcnp3  24435  nmvs  24571  iccntr  24717  reconnlem2  24723  lebnumlem3  24869  caubl  25215  bcthlem5  25235  ovolunlem1  25405  voliunlem1  25458  volsuplem  25463  ellimc3  25787  logbgcd1irr  26711  lgsqrmodndvds  27271  gausslemma2dlem0i  27282  2lgsoddprmlem3  27332  dchrisumlema  27406  nofv  27576  nolesgn2o  27590  nogesgn1o  27592  nosupbnd1lem5  27631  addsprop  27890  negsprop  27948  mulsprop  28040  precsexlem6  28121  precsexlem7  28122  umgrnloopv  29040  usgrnloopvALT  29135  umgrres1lem  29244  upgrres1  29247  nbuhgr  29277  cplgrop  29371  fusgrregdegfi  29504  g0wlk0  29587  wlkdlem2  29618  upgrwlkdvdelem  29673  crctcshwlkn0lem3  29749  crctcshwlkn0lem5  29751  wspn0  29861  umgrwwlks2on  29894  elwspths2spth  29904  clwlkclwwlklem2a  29934  clwlkclwwlklem3  29937  clwwlkn1loopb  29979  clwwlknonwwlknonb  30042  clwwlknonex2lem2  30044  3cyclfrgrrn2  30223  frgrncvvdeqlem8  30242  frgrwopregasn  30252  frgrwopregbsn  30253  frgrwopreg1  30254  frgrwopreg2  30255  frgrregord013  30331  frgrogt3nreg  30333  ablocom  30484  ubthlem1  30806  shaddcl  31153  shmulcl  31154  spansnss2  31511  cnopc  31849  cnfnc  31866  adj1  31869  pjorthcoi  32105  stj  32171  mdsl1i  32257  chirredlem1  32326  mdsymlem5  32343  cdj3lem2b  32373  slmdlema  33163  isprmidlc  33425  pconncn  35218  cvmlift2lem1  35296  fmla0xp  35377  ss2mcls  35562  antnestlaw2  35686  dfon2lem6  35783  waj-ax  36409  lukshef-ax2  36410  bj-alrim  36688  bj-nexdt  36692  sucneqond  37360  rdgssun  37373  ptrecube  37621  poimirlem26  37647  poimirlem29  37650  heiborlem1  37812  rngodm1dm2  37933  rngoueqz  37941  zerdivemp1x  37948  isdrngo3  37960  0rngo  38028  pridl  38038  ispridlc  38071  isdmn3  38075  dmnnzd  38076  elrelscnveq3  38489  lshpcmp  38988  omllaw  39243  dochexmidlem7  41467  lspindp5  41771  zdivgd  42332  fsuppind  42585  dfac21  43062  eexinst11  44524  ax6e2eq  44554  e222  44633  e111  44671  e333  44729  natlocalincr  46881  tworepnotupword  46891  imarnf1pr  47287  2ffzoeq  47332  iccpartigtl  47428  iccpartgt  47432  lighneallem3  47612  lighneal  47616  requad1  47627  evenltle  47722  fppr2odd  47736  sgoldbeven3prm  47788  bgoldbtbndlem2  47811  isubgr3stgrlem4  47972  isubgr3stgrlem7  47975  gpgedg2iv  48062  lincdifsn  48417  lindslinindimp2lem4  48454  snlindsntor  48464  lincresunit3lem1  48472  lincresunit3lem2  48473  f002  48846  setrec1lem2  49681