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  1967  sbequ2OLD  2242  axc16i  2435  eupickbi  2637  ceqsalgALT  3476  cgsexg  3486  cgsex2g  3487  cgsex4g  3488  cgsex4gOLD  3489  spcegv  3551  spc2egv  3553  disjne  4409  uneqdifeq  4445  preqsnd  4811  preq12nebg  4815  opthprneg  4817  dfiun2g  4985  pocl  5546  relresfld  6221  unixpid  6229  ordnbtwn  6403  sucssel  6405  ordelinel  6411  funmo  6508  fvimacnv  6995  2f1fvneq  7198  ordsuc  7735  ordsucOLD  7736  tfi  7776  focdmex  7875  f1ovv  7877  opreuopreu  7953  frrlem4  8184  wfrlem4OLD  8222  wfrlem10OLD  8228  tz7.49  8355  oeworde  8504  fsetprcnex  8730  dom2d  8863  findcard  9037  fisupg  9165  dffi3  9297  noinfep  9526  cantnflem2  9556  ttrcltr  9582  tcmin  9607  rankr1ag  9668  rankunb  9716  rankxpsuc  9748  alephordi  9940  alephsucdom  9945  alephinit  9961  dfac9  10002  ackbij2lem4  10108  cff1  10124  cfslbn  10133  cfcoflem  10138  cfcof  10140  infpssrlem5  10173  isfin7-2  10262  acncc  10306  domtriomlem  10308  axdc3lem2  10317  ttukeylem1  10375  iundom2g  10406  axpowndlem3  10465  wunex2  10604  grupr  10663  gruiun  10665  eltskm  10709  nqereu  10795  addcanpr  10912  axpre-sup  11035  relin01  11609  nneo  12514  zeo2  12517  xrub  13156  uznfz  13449  difelfzle  13479  ssfzo12  13590  facndiv  14112  hashgt12el2  14247  hash2prde  14293  hash2pwpr  14299  hashle2prv  14301  fi1uzind  14320  swrdswrd  14521  pfxccatin12lem2  14547  pfxccatin12  14549  pfxccat3  14550  cshwidxmod  14619  2cshwcshw  14642  fsumcom2  15590  fprodss  15762  fprodcom2  15798  sumodd  16201  ndvdssub  16222  eucalglt  16392  prmind2  16492  coprm  16518  prmdiveq  16589  prmdvdsprmop  16846  prmgaplem5  16858  cicsym  17618  drsdir  18122  lublecllem  18180  istos  18238  tsrlin  18405  dirge  18423  mhmlin  18539  issubg2  18871  nsgbi  18886  symgextf1lem  19129  sylow2a  19325  gsumpr  19655  issubrg2  20153  abvmul  20199  abvtri  20200  lmodlema  20238  rmodislmodlem  20300  rmodislmod  20301  rmodislmodOLD  20302  lspsnel6  20366  lmhmlin  20407  lbsind  20452  0ringnnzr  20650  0ring01eq  20652  01eq0ring  20653  ipcj  20949  obsip  21038  lindsss  21141  mamufacex  21648  mavmulsolcl  21810  slesolvec  21938  inopn  22158  basis1  22210  tgss  22228  tgcl  22229  elcls3  22344  neindisj2  22384  cncls  22535  1stcelcls  22722  qtoptop2  22960  nrmr0reg  23010  fbasssin  23097  fbfinnfr  23102  fbunfip  23130  filufint  23181  uffix  23182  ufinffr  23190  ufilen  23191  fmfnfmlem1  23215  flftg  23257  alexsubALT  23312  xmeteq0  23601  blssexps  23689  blssex  23690  mopni3  23760  neibl  23767  metss  23774  metcnp3  23806  nmvs  23950  iccntr  24094  reconnlem2  24100  lebnumlem3  24236  caubl  24582  bcthlem5  24602  ovolunlem1  24771  voliunlem1  24824  volsuplem  24829  ellimc3  25153  logbgcd1irr  26054  lgsqrmodndvds  26611  gausslemma2dlem0i  26622  2lgsoddprmlem3  26672  dchrisumlema  26746  nofv  26915  nolesgn2o  26929  nogesgn1o  26931  nosupbnd1lem5  26970  umgrnloopv  27831  usgrnloopvALT  27923  umgrres1lem  28032  upgrres1  28035  nbuhgr  28065  cplgrop  28159  fusgrregdegfi  28291  g0wlk0  28374  wlkdlem2  28405  upgrwlkdvdelem  28458  crctcshwlkn0lem3  28531  crctcshwlkn0lem5  28533  wspn0  28643  umgrwwlks2on  28676  elwspths2spth  28686  clwlkclwwlklem2a  28716  clwlkclwwlklem3  28719  clwwlkn1loopb  28761  clwwlknonwwlknonb  28824  clwwlknonex2lem2  28826  3cyclfrgrrn2  29005  frgrncvvdeqlem8  29024  frgrwopregasn  29034  frgrwopregbsn  29035  frgrwopreg1  29036  frgrwopreg2  29037  frgrregord013  29113  frgrogt3nreg  29115  ablocom  29264  ubthlem1  29586  shaddcl  29933  shmulcl  29934  spansnss2  30291  cnopc  30629  cnfnc  30646  adj1  30649  pjorthcoi  30885  stj  30951  mdsl1i  31037  chirredlem1  31106  mdsymlem5  31123  cdj3lem2b  31153  slmdlema  31807  isprmidlc  31984  pconncn  33549  cvmlift2lem1  33627  fmla0xp  33708  ss2mcls  33893  dfon2lem6  34111  addsprop  34242  waj-ax  34742  lukshef-ax2  34743  bj-alrim  35014  bj-nexdt  35018  sucneqond  35692  rdgssun  35705  ptrecube  35933  poimirlem26  35959  poimirlem29  35962  heiborlem1  36125  rngodm1dm2  36246  rngoueqz  36254  zerdivemp1x  36261  isdrngo3  36273  0rngo  36341  pridl  36351  ispridlc  36384  isdmn3  36388  dmnnzd  36389  elrelscnveq3  36809  lshpcmp  37306  omllaw  37561  dochexmidlem7  39785  lspindp5  40089  fsuppind  40590  dfac21  41205  eexinst11  42520  ax6e2eq  42550  e222  42629  e111  42667  e333  42726  natlocalincr  44793  tworepnotupword  44803  imarnf1pr  45192  2ffzoeq  45238  iccpartigtl  45293  iccpartgt  45297  lighneallem3  45477  lighneal  45481  requad1  45492  evenltle  45587  fppr2odd  45601  sgoldbeven3prm  45653  bgoldbtbndlem2  45676  isomuspgrlem2b  45699  nrhmzr  45849  nzerooringczr  46048  lincdifsn  46183  lindslinindimp2lem4  46220  snlindsntor  46230  lincresunit3lem1  46238  lincresunit3lem2  46239  f002  46598  setrec1lem2  46811