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  1968  sbequ2OLD  2245  axc16i  2436  eupickbi  2638  ceqsalgALT  3455  cgsexg  3464  cgsex2g  3465  cgsex4g  3466  cgsex4gOLD  3467  spcegv  3526  spc2egv  3528  disjne  4385  uneqdifeq  4420  preqsnd  4786  preq12nebg  4790  opthprneg  4792  pocl  5501  relresfld  6168  unixpid  6176  ordnbtwn  6341  sucssel  6343  ordelinel  6349  fvimacnv  6912  2f1fvneq  7114  ordsuc  7636  tfi  7675  fornex  7772  f1ovv  7774  opreuopreu  7849  frrlem4  8076  wfrlem4OLD  8114  wfrlem10OLD  8120  tz7.49  8246  oeworde  8386  fsetprcnex  8608  dom2d  8736  findcard  8908  fisupg  8992  dffi3  9120  noinfep  9348  cantnflem2  9378  tcmin  9430  rankr1ag  9491  rankunb  9539  rankxpsuc  9571  alephordi  9761  alephsucdom  9766  alephinit  9782  dfac9  9823  ackbij2lem4  9929  cff1  9945  cfslbn  9954  cfcoflem  9959  cfcof  9961  infpssrlem5  9994  isfin7-2  10083  acncc  10127  domtriomlem  10129  axdc3lem2  10138  ttukeylem1  10196  iundom2g  10227  axpowndlem3  10286  wunex2  10425  grupr  10484  gruiun  10486  eltskm  10530  nqereu  10616  addcanpr  10733  axpre-sup  10856  relin01  11429  nneo  12334  zeo2  12337  xrub  12975  uznfz  13268  difelfzle  13298  ssfzo12  13408  facndiv  13930  hashgt12el2  14066  hash2prde  14112  hash2pwpr  14118  hashle2prv  14120  fi1uzind  14139  swrdswrd  14346  pfxccatin12lem2  14372  pfxccatin12  14374  pfxccat3  14375  cshwidxmod  14444  2cshwcshw  14466  fsumcom2  15414  fprodss  15586  fprodcom2  15622  sumodd  16025  ndvdssub  16046  eucalglt  16218  prmind2  16318  coprm  16344  prmdiveq  16415  prmdvdsprmop  16672  prmgaplem5  16684  cicsym  17433  drsdir  17935  lublecllem  17993  istos  18051  tsrlin  18218  dirge  18236  mhmlin  18352  issubg2  18685  nsgbi  18700  symgextf1lem  18943  sylow2a  19139  gsumpr  19471  issubrg2  19959  abvmul  20004  abvtri  20005  lmodlema  20043  rmodislmodlem  20105  rmodislmod  20106  rmodislmodOLD  20107  lspsnel6  20171  lmhmlin  20212  lbsind  20257  0ringnnzr  20453  0ring01eq  20455  01eq0ring  20456  ipcj  20751  obsip  20838  lindsss  20941  mamufacex  21448  mavmulsolcl  21608  slesolvec  21736  inopn  21956  basis1  22008  tgss  22026  tgcl  22027  elcls3  22142  neindisj2  22182  cncls  22333  1stcelcls  22520  qtoptop2  22758  nrmr0reg  22808  fbasssin  22895  fbfinnfr  22900  fbunfip  22928  filufint  22979  uffix  22980  ufinffr  22988  ufilen  22989  fmfnfmlem1  23013  flftg  23055  alexsubALT  23110  xmeteq0  23399  blssexps  23487  blssex  23488  mopni3  23556  neibl  23563  metss  23570  metcnp3  23602  nmvs  23746  iccntr  23890  reconnlem2  23896  lebnumlem3  24032  caubl  24377  bcthlem5  24397  ovolunlem1  24566  voliunlem1  24619  volsuplem  24624  ellimc3  24948  logbgcd1irr  25849  lgsqrmodndvds  26406  gausslemma2dlem0i  26417  2lgsoddprmlem3  26467  dchrisumlema  26541  umgrnloopv  27379  usgrnloopvALT  27471  umgrres1lem  27580  upgrres1  27583  nbuhgr  27613  cplgrop  27707  fusgrregdegfi  27839  g0wlk0  27921  wlkdlem2  27953  upgrwlkdvdelem  28005  crctcshwlkn0lem3  28078  crctcshwlkn0lem5  28080  wspn0  28190  umgrwwlks2on  28223  elwspths2spth  28233  clwlkclwwlklem2a  28263  clwlkclwwlklem3  28266  clwwlkn1loopb  28308  clwwlknonwwlknonb  28371  clwwlknonex2lem2  28373  3cyclfrgrrn2  28552  frgrncvvdeqlem8  28571  frgrwopregasn  28581  frgrwopregbsn  28582  frgrwopreg1  28583  frgrwopreg2  28584  frgrregord013  28660  frgrogt3nreg  28662  ablocom  28811  ubthlem1  29133  shaddcl  29480  shmulcl  29481  spansnss2  29838  cnopc  30176  cnfnc  30193  adj1  30196  pjorthcoi  30432  stj  30498  mdsl1i  30584  chirredlem1  30653  mdsymlem5  30670  cdj3lem2b  30700  slmdlema  31358  isprmidlc  31525  pconncn  33086  cvmlift2lem1  33164  fmla0xp  33245  ss2mcls  33430  dfon2lem6  33670  ttrcltr  33702  nofv  33787  nolesgn2o  33801  nogesgn1o  33803  nosupbnd1lem5  33842  waj-ax  34530  lukshef-ax2  34531  bj-alrim  34802  bj-nexdt  34806  sucneqond  35463  rdgssun  35476  ptrecube  35704  poimirlem26  35730  poimirlem29  35733  heiborlem1  35896  rngodm1dm2  36017  rngoueqz  36025  zerdivemp1x  36032  isdrngo3  36044  0rngo  36112  pridl  36122  ispridlc  36155  isdmn3  36159  dmnnzd  36160  elrelscnveq3  36536  lshpcmp  36929  omllaw  37184  dochexmidlem7  39407  lspindp5  39711  fsuppind  40202  dfac21  40807  eexinst11  42036  ax6e2eq  42066  e222  42145  e111  42183  e333  42242  imarnf1pr  44661  2ffzoeq  44708  iccpartigtl  44763  iccpartgt  44767  lighneallem3  44947  lighneal  44951  requad1  44962  evenltle  45057  fppr2odd  45071  sgoldbeven3prm  45123  bgoldbtbndlem2  45146  isomuspgrlem2b  45169  nrhmzr  45319  nzerooringczr  45518  lincdifsn  45653  lindslinindimp2lem4  45690  snlindsntor  45700  lincresunit3lem1  45708  lincresunit3lem2  45709  f002  46069  setrec1lem2  46280