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  1982  axc16i  2466  eupickbi  2662  ceqsalgALT  3489  cgsexg  3497  cgsex2g  3498  cgsex4g  3499  spcegv  3556  spc2egv  3558  disjne  4408  uneqdifeq  4445  preqsnd  4816  preq12nebg  4820  opthprneg  4822  dfiun2g  4986  axprlem4  5382  pocl  5561  relresfld  6259  unixpid  6267  ordnbtwn  6437  sucssel  6439  ordelinel  6445  funmo  6533  fvimacnv  7030  ordsuc  7790  tfi  7829  focdmex  7933  f1ovv  7935  opreuopreu  8011  frrlem4  8265  tz7.49  8411  oeworde  8558  fsetprcnex  8839  dom2d  8970  findcard  9128  fisupg  9228  dffi3  9374  noinfep  9612  cantnflem2  9642  ttrcltr  9668  tcmin  9691  rankr1ag  9757  rankunb  9805  rankxpsuc  9837  alephordi  10027  alephsucdom  10032  alephinit  10048  dfac9  10090  ackbij2lem4  10194  cff1  10212  cfslbn  10221  cfcoflem  10226  cfcof  10228  infpssrlem5  10261  isfin7-2  10350  acncc  10394  domtriomlem  10396  axdc3lem2  10405  ttukeylem1  10463  iundom2g  10494  axpowndlem3  10554  wunex2  10693  grupr  10752  gruiun  10754  eltskm  10798  nqereu  10884  addcanpr  11001  axpre-sup  11124  relin01  11708  nneo  12654  zeo2  12657  xrub  13312  uznfz  13612  difelfzle  13643  ssfzo12  13762  facndiv  14298  hashgt12el2  14433  hash2prde  14480  hash2pwpr  14486  hashle2prv  14488  tpfo  14510  fi1uzind  14517  swrdswrd  14715  pfxccatin12lem2  14741  pfxccatin12  14743  pfxccat3  14744  cshwidxmod  14813  2cshwcshw  14835  fsumcom2  15784  fprodss  15961  fprodcom2  15997  sumodd  16405  ndvdssub  16426  eucalglt  16602  prmind2  16702  coprm  16729  prmdiveq  16804  prmdvdsprmop  17062  prmgaplem5  17074  cicsym  17820  drsdir  18317  lublecllem  18373  istos  18431  tsrlin  18600  dirge  18618  mhmlin  18810  issubg2  19166  nsgbi  19181  symgextf1lem  19443  sylow2a  19642  gsumpr  19978  0ringnnzr  20554  0ring01eq  20558  01eq0ringOLD  20560  nrhmzr  20566  issubrng2  20587  issubrg2  20621  abvmul  20850  abvtri  20851  lmodlema  20912  rmodislmodlem  20976  rmodislmod  20977  ellspsn6  21041  lmhmlin  21082  lbsind  21127  nzerooringczr  21512  ipcj  21666  obsip  21753  lindsss  21856  mamufacex  22436  mavmulsolcl  22591  slesolvec  22719  inopn  22939  basis1  22990  tgss  23008  tgcl  23009  elcls3  23123  neindisj2  23163  cncls  23314  1stcelcls  23501  qtoptop2  23739  nrmr0reg  23789  fbasssin  23876  fbfinnfr  23881  fbunfip  23909  filufint  23960  uffix  23961  ufinffr  23969  ufilen  23970  fmfnfmlem1  23994  flftg  24036  alexsubALT  24091  xmeteq0  24378  blssexps  24466  blssex  24467  mopni3  24534  neibl  24541  metss  24548  metcnp3  24580  nmvs  24716  iccntr  24862  reconnlem2  24868  lebnumlem3  25005  caubl  25350  bcthlem5  25370  ovolunlem1  25539  voliunlem1  25592  volsuplem  25597  ellimc3  25921  logbgcd1irr  26836  lgsqrmodndvds  27394  gausslemma2dlem0i  27405  2lgsoddprmlem3  27455  dchrisumlema  27529  nofv  27698  nolesgn2o  27712  nogesgn1o  27714  nosupbnd1lem5  27753  addsprop  28046  negsprop  28105  mulsprop  28200  precsexlem6  28282  precsexlem7  28283  umgrnloopv  29253  usgrnloopvALT  29348  umgrres1lem  29457  upgrres1  29460  nbuhgr  29490  cplgrop  29584  fusgrregdegfi  29716  g0wlk0  29797  wlkdlem2  29828  upgrwlkdvdelem  29882  crctcshwlkn0lem3  29958  crctcshwlkn0lem5  29960  wspn0  30070  usgrwwlks2on  30104  umgrwwlks2on  30105  elwspths2spth  30116  clwlkclwwlklem2a  30146  clwlkclwwlklem3  30149  clwwlkn1loopb  30191  clwwlknonwwlknonb  30254  clwwlknonex2lem2  30256  3cyclfrgrrn2  30435  frgrncvvdeqlem8  30454  frgrwopregasn  30464  frgrwopregbsn  30465  frgrwopreg1  30466  frgrwopreg2  30467  frgrregord013  30543  frgrogt3nreg  30545  ablocom  30697  ubthlem1  31019  shaddcl  31366  shmulcl  31367  spansnss2  31724  cnopc  32062  cnfnc  32079  adj1  32082  pjorthcoi  32318  stj  32384  mdsl1i  32470  chirredlem1  32539  mdsymlem5  32556  cdj3lem2b  32586  slmdlema  33344  isprmidlc  33594  vonf1oonfo  35422  pconncn  35538  cvmlift2lem1  35616  fmla0xp  35697  ss2mcls  35882  antnestlaw2  36006  dfon2lem6  36100  waj-ax  36738  lukshef-ax2  36739  tr0elw  36808  bj-alrim  37132  bj-nexdt  37136  sucneqond  37823  rdgssun  37836  ptrecube  38083  poimirlem26  38109  poimirlem29  38112  heiborlem1  38274  rngodm1dm2  38395  rngoueqz  38403  zerdivemp1x  38410  isdrngo3  38422  0rngo  38490  pridl  38500  ispridlc  38533  isdmn3  38537  dmnnzd  38538  elrelscnveq3  39090  lshpcmp  39576  omllaw  39831  dochexmidlem7  42054  lspindp5  42358  zdivgd  42910  fsuppind  43136  dfac21  43607  eexinst11  45067  ax6e2eq  45097  e222  45176  e111  45214  e333  45272  natlocalincr  47416  imarnf1pr  47840  2ffzoeq  47886  iccpartigtl  47993  iccpartgt  47997  lighneallem3  48180  lighneal  48184  requad1  48208  evenltle  48303  fppr2odd  48317  sgoldbeven3prm  48369  bgoldbtbndlem2  48392  isubgr3stgrlem4  48555  isubgr3stgrlem7  48558  gpgedg2iv  48653  lincdifsn  49010  lindslinindimp2lem4  49047  snlindsntor  49057  lincresunit3lem1  49065  lincresunit3lem2  49066  f002  49439  setrec1lem2  50273