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  2438  eupickbi  2633  ceqsalgALT  3474  cgsexg  3482  cgsex2g  3483  cgsex4g  3484  cgsex4gOLD  3485  spcegv  3548  spc2egv  3550  disjne  4404  uneqdifeq  4442  preqsnd  4810  preq12nebg  4814  opthprneg  4816  dfiun2g  4980  axprlem4  5366  pocl  5535  relresfld  6228  unixpid  6236  ordnbtwn  6406  sucssel  6408  ordelinel  6414  funmo  6502  fvimacnv  6992  ordsuc  7750  tfi  7789  focdmex  7894  f1ovv  7896  opreuopreu  7972  frrlem4  8225  tz7.49  8370  oeworde  8514  fsetprcnex  8792  dom2d  8922  findcard  9080  fisupg  9179  dffi3  9322  noinfep  9557  cantnflem2  9587  ttrcltr  9613  tcmin  9636  rankr1ag  9702  rankunb  9750  rankxpsuc  9782  alephordi  9972  alephsucdom  9977  alephinit  9993  dfac9  10035  ackbij2lem4  10139  cff1  10156  cfslbn  10165  cfcoflem  10170  cfcof  10172  infpssrlem5  10205  isfin7-2  10294  acncc  10338  domtriomlem  10340  axdc3lem2  10349  ttukeylem1  10407  iundom2g  10438  axpowndlem3  10497  wunex2  10636  grupr  10695  gruiun  10697  eltskm  10741  nqereu  10827  addcanpr  10944  axpre-sup  11067  relin01  11648  nneo  12563  zeo2  12566  xrub  13213  uznfz  13512  difelfzle  13543  ssfzo12  13661  facndiv  14197  hashgt12el2  14332  hash2prde  14379  hash2pwpr  14385  hashle2prv  14387  tpfo  14409  fi1uzind  14416  swrdswrd  14614  pfxccatin12lem2  14640  pfxccatin12  14642  pfxccat3  14643  cshwidxmod  14712  2cshwcshw  14734  fsumcom2  15683  fprodss  15857  fprodcom2  15893  sumodd  16301  ndvdssub  16322  eucalglt  16498  prmind2  16598  coprm  16624  prmdiveq  16699  prmdvdsprmop  16957  prmgaplem5  16969  cicsym  17713  drsdir  18210  lublecllem  18266  istos  18324  tsrlin  18493  dirge  18511  mhmlin  18703  issubg2  19056  nsgbi  19071  symgextf1lem  19334  sylow2a  19533  gsumpr  19869  0ringnnzr  20442  0ring01eq  20446  01eq0ringOLD  20448  nrhmzr  20454  issubrng2  20475  issubrg2  20509  abvmul  20738  abvtri  20739  lmodlema  20800  rmodislmodlem  20864  rmodislmod  20865  ellspsn6  20929  lmhmlin  20971  lbsind  21016  nzerooringczr  21419  ipcj  21573  obsip  21660  lindsss  21763  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  29086  usgrnloopvALT  29181  umgrres1lem  29290  upgrres1  29293  nbuhgr  29323  cplgrop  29417  fusgrregdegfi  29550  g0wlk0  29631  wlkdlem2  29662  upgrwlkdvdelem  29716  crctcshwlkn0lem3  29792  crctcshwlkn0lem5  29794  wspn0  29904  usgrwwlks2on  29938  umgrwwlks2on  29939  elwspths2spth  29950  clwlkclwwlklem2a  29980  clwlkclwwlklem3  29983  clwwlkn1loopb  30025  clwwlknonwwlknonb  30088  clwwlknonex2lem2  30090  3cyclfrgrrn2  30269  frgrncvvdeqlem8  30288  frgrwopregasn  30298  frgrwopregbsn  30299  frgrwopreg1  30300  frgrwopreg2  30301  frgrregord013  30377  frgrogt3nreg  30379  ablocom  30530  ubthlem1  30852  shaddcl  31199  shmulcl  31200  spansnss2  31557  cnopc  31895  cnfnc  31912  adj1  31915  pjorthcoi  32151  stj  32217  mdsl1i  32303  chirredlem1  32372  mdsymlem5  32389  cdj3lem2b  32419  slmdlema  33179  isprmidlc  33419  pconncn  35289  cvmlift2lem1  35367  fmla0xp  35448  ss2mcls  35633  antnestlaw2  35757  dfon2lem6  35851  waj-ax  36479  lukshef-ax2  36480  bj-alrim  36758  bj-nexdt  36762  sucneqond  37430  rdgssun  37443  ptrecube  37681  poimirlem26  37707  poimirlem29  37710  heiborlem1  37872  rngodm1dm2  37993  rngoueqz  38001  zerdivemp1x  38008  isdrngo3  38020  0rngo  38088  pridl  38098  ispridlc  38131  isdmn3  38135  dmnnzd  38136  elrelscnveq3  38660  lshpcmp  39108  omllaw  39363  dochexmidlem7  41586  lspindp5  41890  zdivgd  42456  fsuppind  42709  dfac21  43184  eexinst11  44645  ax6e2eq  44675  e222  44754  e111  44792  e333  44850  natlocalincr  46999  imarnf1pr  47407  2ffzoeq  47452  iccpartigtl  47548  iccpartgt  47552  lighneallem3  47732  lighneal  47736  requad1  47747  evenltle  47842  fppr2odd  47856  sgoldbeven3prm  47908  bgoldbtbndlem2  47931  isubgr3stgrlem4  48094  isubgr3stgrlem7  48097  gpgedg2iv  48192  lincdifsn  48550  lindslinindimp2lem4  48587  snlindsntor  48597  lincresunit3lem1  48605  lincresunit3lem2  48606  f002  48979  setrec1lem2  49814