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  1968  sbequ2OLD  2243  axc16i  2437  eupickbi  2639  ceqsalgALT  3466  cgsexg  3475  cgsex2g  3476  cgsex4g  3477  cgsex4gOLD  3478  spcegv  3537  spc2egv  3539  disjne  4389  uneqdifeq  4424  preqsnd  4790  preq12nebg  4794  opthprneg  4796  dfiun2g  4961  pocl  5511  relresfld  6183  unixpid  6191  ordnbtwn  6360  sucssel  6362  ordelinel  6368  funmo  6456  fvimacnv  6939  2f1fvneq  7142  ordsuc  7670  tfi  7709  fornex  7807  f1ovv  7809  opreuopreu  7885  frrlem4  8114  wfrlem4OLD  8152  wfrlem10OLD  8158  tz7.49  8285  oeworde  8433  fsetprcnex  8659  dom2d  8790  findcard  8955  fisupg  9071  dffi3  9199  noinfep  9427  cantnflem2  9457  ttrcltr  9483  tcmin  9508  rankr1ag  9569  rankunb  9617  rankxpsuc  9649  alephordi  9839  alephsucdom  9844  alephinit  9860  dfac9  9901  ackbij2lem4  10007  cff1  10023  cfslbn  10032  cfcoflem  10037  cfcof  10039  infpssrlem5  10072  isfin7-2  10161  acncc  10205  domtriomlem  10207  axdc3lem2  10216  ttukeylem1  10274  iundom2g  10305  axpowndlem3  10364  wunex2  10503  grupr  10562  gruiun  10564  eltskm  10608  nqereu  10694  addcanpr  10811  axpre-sup  10934  relin01  11508  nneo  12413  zeo2  12416  xrub  13055  uznfz  13348  difelfzle  13378  ssfzo12  13489  facndiv  14011  hashgt12el2  14147  hash2prde  14193  hash2pwpr  14199  hashle2prv  14201  fi1uzind  14220  swrdswrd  14427  pfxccatin12lem2  14453  pfxccatin12  14455  pfxccat3  14456  cshwidxmod  14525  2cshwcshw  14547  fsumcom2  15495  fprodss  15667  fprodcom2  15703  sumodd  16106  ndvdssub  16127  eucalglt  16299  prmind2  16399  coprm  16425  prmdiveq  16496  prmdvdsprmop  16753  prmgaplem5  16765  cicsym  17525  drsdir  18029  lublecllem  18087  istos  18145  tsrlin  18312  dirge  18330  mhmlin  18446  issubg2  18779  nsgbi  18794  symgextf1lem  19037  sylow2a  19233  gsumpr  19565  issubrg2  20053  abvmul  20098  abvtri  20099  lmodlema  20137  rmodislmodlem  20199  rmodislmod  20200  rmodislmodOLD  20201  lspsnel6  20265  lmhmlin  20306  lbsind  20351  0ringnnzr  20549  0ring01eq  20551  01eq0ring  20552  ipcj  20848  obsip  20937  lindsss  21040  mamufacex  21547  mavmulsolcl  21709  slesolvec  21837  inopn  22057  basis1  22109  tgss  22127  tgcl  22128  elcls3  22243  neindisj2  22283  cncls  22434  1stcelcls  22621  qtoptop2  22859  nrmr0reg  22909  fbasssin  22996  fbfinnfr  23001  fbunfip  23029  filufint  23080  uffix  23081  ufinffr  23089  ufilen  23090  fmfnfmlem1  23114  flftg  23156  alexsubALT  23211  xmeteq0  23500  blssexps  23588  blssex  23589  mopni3  23659  neibl  23666  metss  23673  metcnp3  23705  nmvs  23849  iccntr  23993  reconnlem2  23999  lebnumlem3  24135  caubl  24481  bcthlem5  24501  ovolunlem1  24670  voliunlem1  24723  volsuplem  24728  ellimc3  25052  logbgcd1irr  25953  lgsqrmodndvds  26510  gausslemma2dlem0i  26521  2lgsoddprmlem3  26571  dchrisumlema  26645  umgrnloopv  27485  usgrnloopvALT  27577  umgrres1lem  27686  upgrres1  27689  nbuhgr  27719  cplgrop  27813  fusgrregdegfi  27945  g0wlk0  28028  wlkdlem2  28060  upgrwlkdvdelem  28113  crctcshwlkn0lem3  28186  crctcshwlkn0lem5  28188  wspn0  28298  umgrwwlks2on  28331  elwspths2spth  28341  clwlkclwwlklem2a  28371  clwlkclwwlklem3  28374  clwwlkn1loopb  28416  clwwlknonwwlknonb  28479  clwwlknonex2lem2  28481  3cyclfrgrrn2  28660  frgrncvvdeqlem8  28679  frgrwopregasn  28689  frgrwopregbsn  28690  frgrwopreg1  28691  frgrwopreg2  28692  frgrregord013  28768  frgrogt3nreg  28770  ablocom  28919  ubthlem1  29241  shaddcl  29588  shmulcl  29589  spansnss2  29946  cnopc  30284  cnfnc  30301  adj1  30304  pjorthcoi  30540  stj  30606  mdsl1i  30692  chirredlem1  30761  mdsymlem5  30778  cdj3lem2b  30808  slmdlema  31465  isprmidlc  31632  pconncn  33195  cvmlift2lem1  33273  fmla0xp  33354  ss2mcls  33539  dfon2lem6  33773  nofv  33869  nolesgn2o  33883  nogesgn1o  33885  nosupbnd1lem5  33924  waj-ax  34612  lukshef-ax2  34613  bj-alrim  34884  bj-nexdt  34888  sucneqond  35545  rdgssun  35558  ptrecube  35786  poimirlem26  35812  poimirlem29  35815  heiborlem1  35978  rngodm1dm2  36099  rngoueqz  36107  zerdivemp1x  36114  isdrngo3  36126  0rngo  36194  pridl  36204  ispridlc  36237  isdmn3  36241  dmnnzd  36242  elrelscnveq3  36616  lshpcmp  37009  omllaw  37264  dochexmidlem7  39487  lspindp5  39791  fsuppind  40286  dfac21  40898  eexinst11  42154  ax6e2eq  42184  e222  42263  e111  42301  e333  42360  imarnf1pr  44785  2ffzoeq  44831  iccpartigtl  44886  iccpartgt  44890  lighneallem3  45070  lighneal  45074  requad1  45085  evenltle  45180  fppr2odd  45194  sgoldbeven3prm  45246  bgoldbtbndlem2  45269  isomuspgrlem2b  45292  nrhmzr  45442  nzerooringczr  45641  lincdifsn  45776  lindslinindimp2lem4  45813  snlindsntor  45823  lincresunit3lem1  45831  lincresunit3lem2  45832  f002  46192  setrec1lem2  46405  natlocalincr  46522  tworepnotupword  46532