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  1966  sbequ2OLD  2251  axc16i  2458  eupickbi  2721  ceqsalgALT  3530  cgsexg  3537  cgsex2g  3538  cgsex4g  3539  spcegv  3597  spc2egv  3600  disjne  4404  uneqdifeq  4438  preqsnd  4789  preq12nebg  4793  opthprneg  4795  relresfld  6127  unixpid  6135  ordnbtwn  6281  sucssel  6283  ordelinel  6289  fvimacnv  6823  2f1fvneq  7018  ordsuc  7529  tfi  7568  fornex  7657  f1ovv  7659  opreuopreu  7734  wfrlem4  7958  wfrlem10  7964  tz7.49  8081  oeworde  8219  dom2d  8550  findcard  8757  fisupg  8766  dffi3  8895  noinfep  9123  cantnflem2  9153  tcmin  9183  rankr1ag  9231  rankunb  9279  rankxpsuc  9311  alephordi  9500  alephsucdom  9505  alephinit  9521  dfac9  9562  ackbij2lem4  9664  cff1  9680  cfslbn  9689  cfcoflem  9694  cfcof  9696  infpssrlem5  9729  isfin7-2  9818  acncc  9862  domtriomlem  9864  axdc3lem2  9873  ttukeylem1  9931  iundom2g  9962  axpowndlem3  10021  wunex2  10160  grupr  10219  gruiun  10221  eltskm  10265  nqereu  10351  addcanpr  10468  axpre-sup  10591  relin01  11164  nneo  12067  zeo2  12070  xrub  12706  uznfz  12991  difelfzle  13021  ssfzo12  13131  facndiv  13649  hashgt12el2  13785  hash2prde  13829  hash2pwpr  13835  hashle2prv  13837  fi1uzind  13856  swrdswrd  14067  pfxccatin12lem2  14093  pfxccatin12  14095  pfxccat3  14096  cshwidxmod  14165  2cshwcshw  14187  relexpcnvd  14395  relexpdmd  14403  relexprnd  14407  relexpfldd  14409  relexpaddd  14413  fsumcom2  15129  fprodss  15302  fprodcom2  15338  sumodd  15739  ndvdssub  15760  eucalglt  15929  prmind2  16029  coprm  16055  prmdiveq  16123  prmdvdsprmop  16379  prmgaplem5  16391  cicsym  17074  drsdir  17545  lublecllem  17598  istos  17645  tsrlin  17829  dirge  17847  mhmlin  17963  issubg2  18294  nsgbi  18309  symgextf1lem  18548  sylow2a  18744  gsumpr  19075  issubrg2  19555  abvmul  19600  abvtri  19601  lmodlema  19639  rmodislmodlem  19701  rmodislmod  19702  lspsnel6  19766  lmhmlin  19807  lbsind  19852  0ringnnzr  20042  0ring01eq  20044  01eq0ring  20045  ipcj  20778  obsip  20865  lindsss  20968  mamufacex  21000  mavmulsolcl  21160  slesolvec  21288  inopn  21507  basis1  21558  tgss  21576  tgcl  21577  elcls3  21691  neindisj2  21731  cncls  21882  1stcelcls  22069  qtoptop2  22307  nrmr0reg  22357  fbasssin  22444  fbfinnfr  22449  fbunfip  22477  filufint  22528  uffix  22529  ufinffr  22537  ufilen  22538  fmfnfmlem1  22562  flftg  22604  alexsubALT  22659  xmeteq0  22948  blssexps  23036  blssex  23037  mopni3  23104  neibl  23111  metss  23118  metcnp3  23150  nmvs  23285  iccntr  23429  reconnlem2  23435  lebnumlem3  23567  caubl  23911  bcthlem5  23931  ovolunlem1  24098  voliunlem1  24151  volsuplem  24156  ellimc3  24477  logbgcd1irr  25372  lgsqrmodndvds  25929  gausslemma2dlem0i  25940  2lgsoddprmlem3  25990  dchrisumlema  26064  umgrnloopv  26891  usgrnloopvALT  26983  umgrres1lem  27092  upgrres1  27095  nbuhgr  27125  cplgrop  27219  fusgrregdegfi  27351  g0wlk0  27433  wlkdlem2  27465  upgrwlkdvdelem  27517  crctcshwlkn0lem3  27590  crctcshwlkn0lem5  27592  wspn0  27703  umgrwwlks2on  27736  elwspths2spth  27746  clwlkclwwlklem2a  27776  clwlkclwwlklem3  27779  clwwlkn1loopb  27821  clwwlknonwwlknonb  27885  clwwlknonex2lem2  27887  3cyclfrgrrn2  28066  frgrncvvdeqlem8  28085  frgrwopregasn  28095  frgrwopregbsn  28096  frgrwopreg1  28097  frgrwopreg2  28098  frgrregord013  28174  frgrogt3nreg  28176  ablocom  28325  ubthlem1  28647  shaddcl  28994  shmulcl  28995  spansnss2  29352  cnopc  29690  cnfnc  29707  adj1  29710  pjorthcoi  29946  stj  30012  mdsl1i  30098  chirredlem1  30167  mdsymlem5  30184  cdj3lem2b  30214  slmdlema  30831  isprmidlc  30963  pconncn  32471  cvmlift2lem1  32549  fmla0xp  32630  ss2mcls  32815  dfon2lem6  33033  frrlem4  33126  nofv  33164  nolesgn2o  33178  nosupbnd1lem5  33212  waj-ax  33762  lukshef-ax2  33763  bj-alrim  34027  bj-nexdt  34031  sucneqond  34649  rdgssun  34662  ptrecube  34907  poimirlem26  34933  poimirlem29  34936  heiborlem1  35104  rngodm1dm2  35225  rngoueqz  35233  zerdivemp1x  35240  isdrngo3  35252  0rngo  35320  pridl  35330  ispridlc  35363  isdmn3  35367  dmnnzd  35368  elrelscnveq3  35746  lshpcmp  36139  omllaw  36394  dochexmidlem7  38617  lspindp5  38921  dfac21  39715  eexinst11  40910  ax6e2eq  40940  e222  41019  e111  41057  e333  41116  imarnf1pr  43530  2ffzoeq  43577  iccpartigtl  43632  iccpartgt  43636  lighneallem3  43821  lighneal  43825  requad1  43836  evenltle  43931  fppr2odd  43945  sgoldbeven3prm  43997  bgoldbtbndlem2  44020  isomuspgrlem2b  44043  nrhmzr  44193  nzerooringczr  44392  lincdifsn  44528  lindslinindimp2lem4  44565  snlindsntor  44575  lincresunit3lem1  44583  lincresunit3lem2  44584  setrec1lem2  44840