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  1964  axc16i  2436  eupickbi  2631  ceqsalgALT  3473  cgsexg  3481  cgsex2g  3482  cgsex4g  3483  cgsex4gOLD  3484  spcegv  3552  spc2egv  3554  disjne  4405  uneqdifeq  4443  preqsnd  4811  preq12nebg  4815  opthprneg  4817  dfiun2g  4980  axprlem4  5364  pocl  5532  relresfld  6223  unixpid  6231  ordnbtwn  6401  sucssel  6403  ordelinel  6409  funmo  6497  fvimacnv  6986  ordsuc  7744  tfi  7783  focdmex  7888  f1ovv  7890  opreuopreu  7966  frrlem4  8219  tz7.49  8364  oeworde  8508  fsetprcnex  8786  dom2d  8915  findcard  9073  fisupg  9172  dffi3  9315  noinfep  9550  cantnflem2  9580  ttrcltr  9606  tcmin  9629  rankr1ag  9695  rankunb  9743  rankxpsuc  9775  alephordi  9965  alephsucdom  9970  alephinit  9986  dfac9  10028  ackbij2lem4  10132  cff1  10149  cfslbn  10158  cfcoflem  10163  cfcof  10165  infpssrlem5  10198  isfin7-2  10287  acncc  10331  domtriomlem  10333  axdc3lem2  10342  ttukeylem1  10400  iundom2g  10431  axpowndlem3  10490  wunex2  10629  grupr  10688  gruiun  10690  eltskm  10734  nqereu  10820  addcanpr  10937  axpre-sup  11060  relin01  11641  nneo  12557  zeo2  12560  xrub  13211  uznfz  13510  difelfzle  13541  ssfzo12  13659  facndiv  14195  hashgt12el2  14330  hash2prde  14377  hash2pwpr  14383  hashle2prv  14385  tpfo  14407  fi1uzind  14414  swrdswrd  14612  pfxccatin12lem2  14638  pfxccatin12  14640  pfxccat3  14641  cshwidxmod  14710  2cshwcshw  14732  fsumcom2  15681  fprodss  15855  fprodcom2  15891  sumodd  16299  ndvdssub  16320  eucalglt  16496  prmind2  16596  coprm  16622  prmdiveq  16697  prmdvdsprmop  16955  prmgaplem5  16967  cicsym  17711  drsdir  18208  lublecllem  18264  istos  18322  tsrlin  18491  dirge  18509  mhmlin  18701  issubg2  19054  nsgbi  19070  symgextf1lem  19333  sylow2a  19532  gsumpr  19868  0ringnnzr  20441  0ring01eq  20445  01eq0ringOLD  20447  nrhmzr  20453  issubrng2  20474  issubrg2  20508  abvmul  20737  abvtri  20738  lmodlema  20799  rmodislmodlem  20863  rmodislmod  20864  ellspsn6  20928  lmhmlin  20970  lbsind  21015  nzerooringczr  21418  ipcj  21572  obsip  21659  lindsss  21762  mamufacex  22312  mavmulsolcl  22467  slesolvec  22595  inopn  22815  basis1  22866  tgss  22884  tgcl  22885  elcls3  22999  neindisj2  23039  cncls  23190  1stcelcls  23377  qtoptop2  23615  nrmr0reg  23665  fbasssin  23752  fbfinnfr  23757  fbunfip  23785  filufint  23836  uffix  23837  ufinffr  23845  ufilen  23846  fmfnfmlem1  23870  flftg  23912  alexsubALT  23967  xmeteq0  24254  blssexps  24342  blssex  24343  mopni3  24410  neibl  24417  metss  24424  metcnp3  24456  nmvs  24592  iccntr  24738  reconnlem2  24744  lebnumlem3  24890  caubl  25236  bcthlem5  25256  ovolunlem1  25426  voliunlem1  25479  volsuplem  25484  ellimc3  25808  logbgcd1irr  26732  lgsqrmodndvds  27292  gausslemma2dlem0i  27303  2lgsoddprmlem3  27353  dchrisumlema  27427  nofv  27597  nolesgn2o  27611  nogesgn1o  27613  nosupbnd1lem5  27652  addsprop  27920  negsprop  27978  mulsprop  28070  precsexlem6  28151  precsexlem7  28152  umgrnloopv  29085  usgrnloopvALT  29180  umgrres1lem  29289  upgrres1  29292  nbuhgr  29322  cplgrop  29416  fusgrregdegfi  29549  g0wlk0  29630  wlkdlem2  29661  upgrwlkdvdelem  29715  crctcshwlkn0lem3  29791  crctcshwlkn0lem5  29793  wspn0  29903  umgrwwlks2on  29936  elwspths2spth  29946  clwlkclwwlklem2a  29976  clwlkclwwlklem3  29979  clwwlkn1loopb  30021  clwwlknonwwlknonb  30084  clwwlknonex2lem2  30086  3cyclfrgrrn2  30265  frgrncvvdeqlem8  30284  frgrwopregasn  30294  frgrwopregbsn  30295  frgrwopreg1  30296  frgrwopreg2  30297  frgrregord013  30373  frgrogt3nreg  30375  ablocom  30526  ubthlem1  30848  shaddcl  31195  shmulcl  31196  spansnss2  31553  cnopc  31891  cnfnc  31908  adj1  31911  pjorthcoi  32147  stj  32213  mdsl1i  32299  chirredlem1  32368  mdsymlem5  32385  cdj3lem2b  32415  slmdlema  33170  isprmidlc  33410  pconncn  35266  cvmlift2lem1  35344  fmla0xp  35425  ss2mcls  35610  antnestlaw2  35734  dfon2lem6  35828  waj-ax  36454  lukshef-ax2  36455  bj-alrim  36733  bj-nexdt  36737  sucneqond  37405  rdgssun  37418  ptrecube  37666  poimirlem26  37692  poimirlem29  37695  heiborlem1  37857  rngodm1dm2  37978  rngoueqz  37986  zerdivemp1x  37993  isdrngo3  38005  0rngo  38073  pridl  38083  ispridlc  38116  isdmn3  38120  dmnnzd  38121  elrelscnveq3  38534  lshpcmp  39033  omllaw  39288  dochexmidlem7  41511  lspindp5  41815  zdivgd  42376  fsuppind  42629  dfac21  43105  eexinst11  44566  ax6e2eq  44596  e222  44675  e111  44713  e333  44771  natlocalincr  46920  imarnf1pr  47319  2ffzoeq  47364  iccpartigtl  47460  iccpartgt  47464  lighneallem3  47644  lighneal  47648  requad1  47659  evenltle  47754  fppr2odd  47768  sgoldbeven3prm  47820  bgoldbtbndlem2  47843  isubgr3stgrlem4  48006  isubgr3stgrlem7  48009  gpgedg2iv  48104  lincdifsn  48462  lindslinindimp2lem4  48499  snlindsntor  48509  lincresunit3lem1  48517  lincresunit3lem2  48518  f002  48891  setrec1lem2  49726