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  1965  axc16i  2440  eupickbi  2636  ceqsalgALT  3466  cgsexg  3474  cgsex2g  3475  cgsex4g  3476  spcegv  3539  spc2egv  3541  disjne  4395  uneqdifeq  4432  preqsnd  4802  preq12nebg  4806  opthprneg  4808  dfiun2g  4972  axprlem4  5368  pocl  5547  relresfld  6240  unixpid  6248  ordnbtwn  6418  sucssel  6420  ordelinel  6426  funmo  6514  fvimacnv  7005  ordsuc  7765  tfi  7804  focdmex  7909  f1ovv  7911  opreuopreu  7987  frrlem4  8239  tz7.49  8384  oeworde  8529  fsetprcnex  8809  dom2d  8940  findcard  9098  fisupg  9198  dffi3  9344  noinfep  9581  cantnflem2  9611  ttrcltr  9637  tcmin  9660  rankr1ag  9726  rankunb  9774  rankxpsuc  9806  alephordi  9996  alephsucdom  10001  alephinit  10017  dfac9  10059  ackbij2lem4  10163  cff1  10180  cfslbn  10189  cfcoflem  10194  cfcof  10196  infpssrlem5  10229  isfin7-2  10318  acncc  10362  domtriomlem  10364  axdc3lem2  10373  ttukeylem1  10431  iundom2g  10462  axpowndlem3  10522  wunex2  10661  grupr  10720  gruiun  10722  eltskm  10766  nqereu  10852  addcanpr  10969  axpre-sup  11092  relin01  11674  nneo  12613  zeo2  12616  xrub  13264  uznfz  13564  difelfzle  13595  ssfzo12  13714  facndiv  14250  hashgt12el2  14385  hash2prde  14432  hash2pwpr  14438  hashle2prv  14440  tpfo  14462  fi1uzind  14469  swrdswrd  14667  pfxccatin12lem2  14693  pfxccatin12  14695  pfxccat3  14696  cshwidxmod  14765  2cshwcshw  14787  fsumcom2  15736  fprodss  15913  fprodcom2  15949  sumodd  16357  ndvdssub  16378  eucalglt  16554  prmind2  16654  coprm  16681  prmdiveq  16756  prmdvdsprmop  17014  prmgaplem5  17026  cicsym  17771  drsdir  18268  lublecllem  18324  istos  18382  tsrlin  18551  dirge  18569  mhmlin  18761  issubg2  19117  nsgbi  19132  symgextf1lem  19395  sylow2a  19594  gsumpr  19930  0ringnnzr  20502  0ring01eq  20506  01eq0ringOLD  20508  nrhmzr  20514  issubrng2  20535  issubrg2  20569  abvmul  20798  abvtri  20799  lmodlema  20860  rmodislmodlem  20924  rmodislmod  20925  ellspsn6  20989  lmhmlin  21030  lbsind  21075  nzerooringczr  21460  ipcj  21614  obsip  21701  lindsss  21804  mamufacex  22361  mavmulsolcl  22516  slesolvec  22644  inopn  22864  basis1  22915  tgss  22933  tgcl  22934  elcls3  23048  neindisj2  23088  cncls  23239  1stcelcls  23426  qtoptop2  23664  nrmr0reg  23714  fbasssin  23801  fbfinnfr  23806  fbunfip  23834  filufint  23885  uffix  23886  ufinffr  23894  ufilen  23895  fmfnfmlem1  23919  flftg  23961  alexsubALT  24016  xmeteq0  24303  blssexps  24391  blssex  24392  mopni3  24459  neibl  24466  metss  24473  metcnp3  24505  nmvs  24641  iccntr  24787  reconnlem2  24793  lebnumlem3  24930  caubl  25275  bcthlem5  25295  ovolunlem1  25464  voliunlem1  25517  volsuplem  25522  ellimc3  25846  logbgcd1irr  26758  lgsqrmodndvds  27316  gausslemma2dlem0i  27327  2lgsoddprmlem3  27377  dchrisumlema  27451  nofv  27621  nolesgn2o  27635  nogesgn1o  27637  nosupbnd1lem5  27676  addsprop  27968  negsprop  28027  mulsprop  28122  precsexlem6  28204  precsexlem7  28205  umgrnloopv  29175  usgrnloopvALT  29270  umgrres1lem  29379  upgrres1  29382  nbuhgr  29412  cplgrop  29506  fusgrregdegfi  29638  g0wlk0  29719  wlkdlem2  29750  upgrwlkdvdelem  29804  crctcshwlkn0lem3  29880  crctcshwlkn0lem5  29882  wspn0  29992  usgrwwlks2on  30026  umgrwwlks2on  30027  elwspths2spth  30038  clwlkclwwlklem2a  30068  clwlkclwwlklem3  30071  clwwlkn1loopb  30113  clwwlknonwwlknonb  30176  clwwlknonex2lem2  30178  3cyclfrgrrn2  30357  frgrncvvdeqlem8  30376  frgrwopregasn  30386  frgrwopregbsn  30387  frgrwopreg1  30388  frgrwopreg2  30389  frgrregord013  30465  frgrogt3nreg  30467  ablocom  30619  ubthlem1  30941  shaddcl  31288  shmulcl  31289  spansnss2  31646  cnopc  31984  cnfnc  32001  adj1  32004  pjorthcoi  32240  stj  32306  mdsl1i  32392  chirredlem1  32461  mdsymlem5  32478  cdj3lem2b  32508  slmdlema  33264  isprmidlc  33507  pconncn  35406  cvmlift2lem1  35484  fmla0xp  35565  ss2mcls  35750  antnestlaw2  35874  dfon2lem6  35968  waj-ax  36596  lukshef-ax2  36597  tr0elw  36666  bj-alrim  36990  bj-nexdt  36994  sucneqond  37681  rdgssun  37694  ptrecube  37941  poimirlem26  37967  poimirlem29  37970  heiborlem1  38132  rngodm1dm2  38253  rngoueqz  38261  zerdivemp1x  38268  isdrngo3  38280  0rngo  38348  pridl  38358  ispridlc  38391  isdmn3  38395  dmnnzd  38396  elrelscnveq3  38948  lshpcmp  39434  omllaw  39689  dochexmidlem7  41912  lspindp5  42216  zdivgd  42769  fsuppind  43023  dfac21  43494  eexinst11  44954  ax6e2eq  44984  e222  45063  e111  45101  e333  45159  natlocalincr  47306  imarnf1pr  47730  2ffzoeq  47776  iccpartigtl  47883  iccpartgt  47887  lighneallem3  48070  lighneal  48074  requad1  48098  evenltle  48193  fppr2odd  48207  sgoldbeven3prm  48259  bgoldbtbndlem2  48282  isubgr3stgrlem4  48445  isubgr3stgrlem7  48448  gpgedg2iv  48543  lincdifsn  48900  lindslinindimp2lem4  48937  snlindsntor  48947  lincresunit3lem1  48955  lincresunit3lem2  48956  f002  49329  setrec1lem2  50163