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  2441  eupickbi  2636  ceqsalgALT  3518  cgsexg  3526  cgsex2g  3527  cgsex4g  3528  cgsex4gOLD  3529  spcegv  3597  spc2egv  3599  disjne  4455  uneqdifeq  4493  preqsnd  4859  preq12nebg  4863  opthprneg  4865  dfiun2g  5030  axprlem4  5426  pocl  5600  relresfld  6296  unixpid  6304  ordnbtwn  6477  sucssel  6479  ordelinel  6485  funmo  6581  fvimacnv  7073  2f1fvneq  7280  ordsuc  7833  ordsucOLD  7834  tfi  7874  focdmex  7980  f1ovv  7982  opreuopreu  8059  frrlem4  8314  wfrlem4OLD  8352  wfrlem10OLD  8358  tz7.49  8485  oeworde  8631  fsetprcnex  8902  dom2d  9033  findcard  9203  fisupg  9324  dffi3  9471  noinfep  9700  cantnflem2  9730  ttrcltr  9756  tcmin  9781  rankr1ag  9842  rankunb  9890  rankxpsuc  9922  alephordi  10114  alephsucdom  10119  alephinit  10135  dfac9  10177  ackbij2lem4  10281  cff1  10298  cfslbn  10307  cfcoflem  10312  cfcof  10314  infpssrlem5  10347  isfin7-2  10436  acncc  10480  domtriomlem  10482  axdc3lem2  10491  ttukeylem1  10549  iundom2g  10580  axpowndlem3  10639  wunex2  10778  grupr  10837  gruiun  10839  eltskm  10883  nqereu  10969  addcanpr  11086  axpre-sup  11209  relin01  11787  nneo  12702  zeo2  12705  xrub  13354  uznfz  13650  difelfzle  13681  ssfzo12  13798  facndiv  14327  hashgt12el2  14462  hash2prde  14509  hash2pwpr  14515  hashle2prv  14517  tpfo  14539  fi1uzind  14546  swrdswrd  14743  pfxccatin12lem2  14769  pfxccatin12  14771  pfxccat3  14772  cshwidxmod  14841  2cshwcshw  14864  fsumcom2  15810  fprodss  15984  fprodcom2  16020  sumodd  16425  ndvdssub  16446  eucalglt  16622  prmind2  16722  coprm  16748  prmdiveq  16823  prmdvdsprmop  17081  prmgaplem5  17093  cicsym  17848  drsdir  18348  lublecllem  18405  istos  18463  tsrlin  18630  dirge  18648  mhmlin  18806  issubg2  19159  nsgbi  19175  symgextf1lem  19438  sylow2a  19637  gsumpr  19973  0ringnnzr  20525  0ring01eq  20529  01eq0ringOLD  20531  nrhmzr  20537  issubrng2  20558  issubrg2  20592  abvmul  20822  abvtri  20823  lmodlema  20863  rmodislmodlem  20927  rmodislmod  20928  ellspsn6  20992  lmhmlin  21034  lbsind  21079  nzerooringczr  21491  ipcj  21652  obsip  21741  lindsss  21844  mamufacex  22400  mavmulsolcl  22557  slesolvec  22685  inopn  22905  basis1  22957  tgss  22975  tgcl  22976  elcls3  23091  neindisj2  23131  cncls  23282  1stcelcls  23469  qtoptop2  23707  nrmr0reg  23757  fbasssin  23844  fbfinnfr  23849  fbunfip  23877  filufint  23928  uffix  23929  ufinffr  23937  ufilen  23938  fmfnfmlem1  23962  flftg  24004  alexsubALT  24059  xmeteq0  24348  blssexps  24436  blssex  24437  mopni3  24507  neibl  24514  metss  24521  metcnp3  24553  nmvs  24697  iccntr  24843  reconnlem2  24849  lebnumlem3  24995  caubl  25342  bcthlem5  25362  ovolunlem1  25532  voliunlem1  25585  volsuplem  25590  ellimc3  25914  logbgcd1irr  26837  lgsqrmodndvds  27397  gausslemma2dlem0i  27408  2lgsoddprmlem3  27458  dchrisumlema  27532  nofv  27702  nolesgn2o  27716  nogesgn1o  27718  nosupbnd1lem5  27757  addsprop  28009  negsprop  28067  mulsprop  28156  precsexlem6  28236  precsexlem7  28237  umgrnloopv  29123  usgrnloopvALT  29218  umgrres1lem  29327  upgrres1  29330  nbuhgr  29360  cplgrop  29454  fusgrregdegfi  29587  g0wlk0  29670  wlkdlem2  29701  upgrwlkdvdelem  29756  crctcshwlkn0lem3  29832  crctcshwlkn0lem5  29834  wspn0  29944  umgrwwlks2on  29977  elwspths2spth  29987  clwlkclwwlklem2a  30017  clwlkclwwlklem3  30020  clwwlkn1loopb  30062  clwwlknonwwlknonb  30125  clwwlknonex2lem2  30127  3cyclfrgrrn2  30306  frgrncvvdeqlem8  30325  frgrwopregasn  30335  frgrwopregbsn  30336  frgrwopreg1  30337  frgrwopreg2  30338  frgrregord013  30414  frgrogt3nreg  30416  ablocom  30567  ubthlem1  30889  shaddcl  31236  shmulcl  31237  spansnss2  31594  cnopc  31932  cnfnc  31949  adj1  31952  pjorthcoi  32188  stj  32254  mdsl1i  32340  chirredlem1  32409  mdsymlem5  32426  cdj3lem2b  32456  slmdlema  33209  isprmidlc  33475  pconncn  35229  cvmlift2lem1  35307  fmla0xp  35388  ss2mcls  35573  dfon2lem6  35789  waj-ax  36415  lukshef-ax2  36416  bj-alrim  36694  bj-nexdt  36698  sucneqond  37366  rdgssun  37379  ptrecube  37627  poimirlem26  37653  poimirlem29  37656  heiborlem1  37818  rngodm1dm2  37939  rngoueqz  37947  zerdivemp1x  37954  isdrngo3  37966  0rngo  38034  pridl  38044  ispridlc  38077  isdmn3  38081  dmnnzd  38082  elrelscnveq3  38492  lshpcmp  38989  omllaw  39244  dochexmidlem7  41468  lspindp5  41772  zdivgd  42372  fsuppind  42600  dfac21  43078  eexinst11  44547  ax6e2eq  44577  e222  44656  e111  44694  e333  44753  natlocalincr  46891  tworepnotupword  46901  imarnf1pr  47294  2ffzoeq  47339  iccpartigtl  47410  iccpartgt  47414  lighneallem3  47594  lighneal  47598  requad1  47609  evenltle  47704  fppr2odd  47718  sgoldbeven3prm  47770  bgoldbtbndlem2  47793  isubgr3stgrlem4  47936  isubgr3stgrlem7  47939  lincdifsn  48341  lindslinindimp2lem4  48378  snlindsntor  48388  lincresunit3lem1  48396  lincresunit3lem2  48397  f002  48763  setrec1lem2  49207