Theorem syl5com 32

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 26	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
3		syl5com.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	sylcom 31	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  33  syl5  35  speimfw  1986  axc16i  2470  eupickbi  2666  ceqsalgALT  3493  cgsexg  3501  cgsex2g  3502  cgsex4g  3503  spcegv  3559  spc2egv  3561  disjne  4412  uneqdifeq  4449  preqsnd  4819  preq12nebg  4823  opthprneg  4825  dfiun2g  4989  axprlem4  5387  pocl  5567  relresfld  6266  unixpid  6274  ordnbtwn  6445  sucssel  6447  ordelinel  6453  funmo  6541  fvimacnv  7038  ordsuc  7798  tfi  7837  focdmex  7941  f1ovv  7943  opreuopreu  8019  frrlem4  8274  tz7.49  8420  oeworde  8567  fsetprcnex  8847  dom2d  8978  findcard  9136  fisupg  9236  dffi3  9379  noinfep  9617  cantnflem2  9647  ttrcltr  9673  tcmin  9696  rankr1ag  9762  rankunb  9810  rankxpsuc  9842  alephordi  10046  alephsucdom  10051  alephinit  10067  dfac9  10108  ackbij2lem4  10212  cff1  10230  cfslbn  10239  cfcoflem  10244  cfcof  10246  infpssrlem5  10279  isfin7-2  10368  acncc  10412  domtriomlem  10414  axdc3lem2  10423  ttukeylem1  10481  iundom2g  10512  axpowndlem3  10572  wunex2  10711  grupr  10770  gruiun  10772  eltskm  10816  nqereu  10902  addcanpr  11019  axpre-sup  11142  relin01  11726  nneo  12668  zeo2  12671  xrub  13326  uznfz  13626  difelfzle  13657  ssfzo12  13776  facndiv  14312  hashgt12el2  14448  hash2prde  14495  hash2pwpr  14501  hashle2prv  14503  tpfo  14525  fi1uzind  14532  swrdswrd  14730  pfxccatin12lem2  14756  pfxccatin12  14758  pfxccat3  14759  cshwidxmod  14828  2cshwcshw  14850  fsumcom2  15813  fprodss  15990  fprodcom2  16026  sumodd  16434  ndvdssub  16455  eucalglt  16631  prmind2  16731  coprm  16758  prmdiveq  16833  prmdvdsprmop  17091  prmgaplem5  17103  cicsym  17849  drsdir  18346  lublecllem  18402  istos  18460  tsrlin  18629  dirge  18647  mhmlin  18839  issubg2  19196  nsgbi  19211  symgextf1lem  19478  sylow2a  19677  gsumpr  20013  0ringnnzr  20597  0ring01eq  20601  01eq0ringOLD  20603  nrhmzr  20610  issubrng2  20631  issubrg2  20665  abvmul  20890  abvtri  20891  lmodlema  20952  rmodislmodlem  21016  rmodislmod  21017  ellspsn6  21081  lmhmlin  21122  lbsind  21167  isprmidlc  21431  nzerooringczr  21587  ipcj  21741  obsip  21828  lindsss  21931  mamufacex  22510  mavmulsolcl  22665  slesolvec  22793  inopn  23013  basis1  23064  tgss  23082  tgcl  23083  elcls3  23197  neindisj2  23237  cncls  23388  1stcelcls  23575  qtoptop2  23813  nrmr0reg  23863  fbasssin  23950  fbfinnfr  23955  fbunfip  23983  filufint  24034  uffix  24035  ufinffr  24043  ufilen  24044  fmfnfmlem1  24068  flftg  24110  alexsubALT  24165  xmeteq0  24452  blssexps  24540  blssex  24541  mopni3  24608  neibl  24615  metss  24622  metcnp3  24654  nmvs  24790  iccntr  24936  reconnlem2  24942  lebnumlem3  25079  caubl  25424  bcthlem5  25444  ovolunlem1  25613  voliunlem1  25666  volsuplem  25671  ellimc3  25995  logbgcd1irr  26913  lgsqrmodndvds  27471  gausslemma2dlem0i  27482  2lgsoddprmlem3  27532  dchrisumlema  27606  nofv  27775  nolesgn2o  27789  nogesgn1o  27791  nosupbnd1lem5  27830  addsprop  28123  negsprop  28182  mulsprop  28277  precsexlem6  28359  precsexlem7  28360  umgrnloopv  29361  usgrnloopvALT  29456  umgrres1lem  29565  upgrres1  29568  nbuhgr  29598  cplgrop  29692  fusgrregdegfi  29824  g0wlk0  29905  wlkdlem2  29936  upgrwlkdvdelem  29990  crctcshwlkn0lem3  30066  crctcshwlkn0lem5  30068  wspn0  30178  usgrwwlks2on  30212  umgrwwlks2on  30213  elwspths2spth  30224  clwlkclwwlklem2a  30254  clwlkclwwlklem3  30257  clwwlkn1loopb  30299  clwwlknonwwlknonb  30362  clwwlknonex2lem2  30364  3cyclfrgrrn2  30543  frgrncvvdeqlem8  30562  frgrwopregasn  30572  frgrwopregbsn  30573  frgrwopreg1  30574  frgrwopreg2  30575  frgrregord013  30651  frgrogt3nreg  30653  ablocom  30805  ubthlem1  31127  shaddcl  31474  shmulcl  31475  spansnss2  31832  cnopc  32170  cnfnc  32187  adj1  32190  pjorthcoi  32426  stj  32492  mdsl1i  32578  chirredlem1  32647  mdsymlem5  32664  cdj3lem2b  32694  slmdlema  33431  vonf1oonfo  35465  pconncn  35582  cvmlift2lem1  35660  fmla0xp  35741  ss2mcls  35926  antnestlaw2  36050  dfon2lem6  36144  waj-ax  36782  lukshef-ax2  36783  tr0elw  36852  bj-alrim  37175  bj-nexdt  37179  sucneqond  37866  rdgssun  37879  ptrecube  38126  poimirlem26  38152  poimirlem29  38155  heiborlem1  38317  rngodm1dm2  38438  rngoueqz  38446  zerdivemp1x  38453  isdrngo3  38465  0rngo  38533  pridl  38543  ispridlc  38576  isdmn3  38580  dmnnzd  38581  elrelscnveq3  39133  lshpcmp  39619  omllaw  39874  dochexmidlem7  42097  lspindp5  42401  zdivgd  42953  fsuppind  43179  dfac21  43650  eexinst11  45095  ax6e2eq  45125  e222  45204  e111  45242  e333  45300  natlocalincr  47451  imarnf1pr  47875  2ffzoeq  47921  iccpartigtl  48028  iccpartgt  48032  lighneallem3  48215  lighneal  48219  requad1  48243  evenltle  48338  fppr2odd  48352  sgoldbeven3prm  48404  bgoldbtbndlem2  48427  isubgr3stgrlem4  48590  isubgr3stgrlem7  48593  gpgedg2iv  48688  lincdifsn  49056  lindslinindimp2lem4  49093  snlindsntor  49103  lincresunit3lem1  49111  lincresunit3lem2  49112  f002  49484  setrec1lem2  50318