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  1963  axc16i  2444  eupickbi  2639  ceqsalgALT  3526  cgsexg  3536  cgsex2g  3537  cgsex4g  3538  cgsex4gOLD  3539  spcegv  3610  spc2egv  3612  disjne  4478  uneqdifeq  4516  preqsnd  4883  preq12nebg  4887  opthprneg  4889  dfiun2g  5053  pocl  5615  relresfld  6307  unixpid  6315  ordnbtwn  6488  sucssel  6490  ordelinel  6496  funmo  6593  fvimacnv  7086  2f1fvneq  7297  ordsuc  7849  ordsucOLD  7850  tfi  7890  focdmex  7996  f1ovv  7998  opreuopreu  8075  frrlem4  8330  wfrlem4OLD  8368  wfrlem10OLD  8374  tz7.49  8501  oeworde  8649  fsetprcnex  8920  dom2d  9053  findcard  9229  fisupg  9352  dffi3  9500  noinfep  9729  cantnflem2  9759  ttrcltr  9785  tcmin  9810  rankr1ag  9871  rankunb  9919  rankxpsuc  9951  alephordi  10143  alephsucdom  10148  alephinit  10164  dfac9  10206  ackbij2lem4  10310  cff1  10327  cfslbn  10336  cfcoflem  10341  cfcof  10343  infpssrlem5  10376  isfin7-2  10465  acncc  10509  domtriomlem  10511  axdc3lem2  10520  ttukeylem1  10578  iundom2g  10609  axpowndlem3  10668  wunex2  10807  grupr  10866  gruiun  10868  eltskm  10912  nqereu  10998  addcanpr  11115  axpre-sup  11238  relin01  11814  nneo  12727  zeo2  12730  xrub  13374  uznfz  13667  difelfzle  13698  ssfzo12  13809  facndiv  14337  hashgt12el2  14472  hash2prde  14519  hash2pwpr  14525  hashle2prv  14527  tpfo  14549  fi1uzind  14556  swrdswrd  14753  pfxccatin12lem2  14779  pfxccatin12  14781  pfxccat3  14782  cshwidxmod  14851  2cshwcshw  14874  fsumcom2  15822  fprodss  15996  fprodcom2  16032  sumodd  16436  ndvdssub  16457  eucalglt  16632  prmind2  16732  coprm  16758  prmdiveq  16833  prmdvdsprmop  17090  prmgaplem5  17102  cicsym  17865  drsdir  18372  lublecllem  18430  istos  18488  tsrlin  18655  dirge  18673  mhmlin  18828  issubg2  19181  nsgbi  19197  symgextf1lem  19462  sylow2a  19661  gsumpr  19997  0ringnnzr  20551  0ring01eq  20555  01eq0ringOLD  20557  nrhmzr  20563  issubrng2  20584  issubrg2  20620  abvmul  20844  abvtri  20845  lmodlema  20885  rmodislmodlem  20949  rmodislmod  20950  rmodislmodOLD  20951  ellspsn6  21015  lmhmlin  21057  lbsind  21102  nzerooringczr  21514  ipcj  21675  obsip  21764  lindsss  21867  mamufacex  22421  mavmulsolcl  22578  slesolvec  22706  inopn  22926  basis1  22978  tgss  22996  tgcl  22997  elcls3  23112  neindisj2  23152  cncls  23303  1stcelcls  23490  qtoptop2  23728  nrmr0reg  23778  fbasssin  23865  fbfinnfr  23870  fbunfip  23898  filufint  23949  uffix  23950  ufinffr  23958  ufilen  23959  fmfnfmlem1  23983  flftg  24025  alexsubALT  24080  xmeteq0  24369  blssexps  24457  blssex  24458  mopni3  24528  neibl  24535  metss  24542  metcnp3  24574  nmvs  24718  iccntr  24862  reconnlem2  24868  lebnumlem3  25014  caubl  25361  bcthlem5  25381  ovolunlem1  25551  voliunlem1  25604  volsuplem  25609  ellimc3  25934  logbgcd1irr  26855  lgsqrmodndvds  27415  gausslemma2dlem0i  27426  2lgsoddprmlem3  27476  dchrisumlema  27550  nofv  27720  nolesgn2o  27734  nogesgn1o  27736  nosupbnd1lem5  27775  addsprop  28027  negsprop  28085  mulsprop  28174  precsexlem6  28254  precsexlem7  28255  umgrnloopv  29141  usgrnloopvALT  29236  umgrres1lem  29345  upgrres1  29348  nbuhgr  29378  cplgrop  29472  fusgrregdegfi  29605  g0wlk0  29688  wlkdlem2  29719  upgrwlkdvdelem  29772  crctcshwlkn0lem3  29845  crctcshwlkn0lem5  29847  wspn0  29957  umgrwwlks2on  29990  elwspths2spth  30000  clwlkclwwlklem2a  30030  clwlkclwwlklem3  30033  clwwlkn1loopb  30075  clwwlknonwwlknonb  30138  clwwlknonex2lem2  30140  3cyclfrgrrn2  30319  frgrncvvdeqlem8  30338  frgrwopregasn  30348  frgrwopregbsn  30349  frgrwopreg1  30350  frgrwopreg2  30351  frgrregord013  30427  frgrogt3nreg  30429  ablocom  30580  ubthlem1  30902  shaddcl  31249  shmulcl  31250  spansnss2  31607  cnopc  31945  cnfnc  31962  adj1  31965  pjorthcoi  32201  stj  32267  mdsl1i  32353  chirredlem1  32422  mdsymlem5  32439  cdj3lem2b  32469  slmdlema  33182  isprmidlc  33440  pconncn  35192  cvmlift2lem1  35270  fmla0xp  35351  ss2mcls  35536  dfon2lem6  35752  waj-ax  36380  lukshef-ax2  36381  bj-alrim  36659  bj-nexdt  36663  sucneqond  37331  rdgssun  37344  ptrecube  37580  poimirlem26  37606  poimirlem29  37609  heiborlem1  37771  rngodm1dm2  37892  rngoueqz  37900  zerdivemp1x  37907  isdrngo3  37919  0rngo  37987  pridl  37997  ispridlc  38030  isdmn3  38034  dmnnzd  38035  elrelscnveq3  38447  lshpcmp  38944  omllaw  39199  dochexmidlem7  41423  lspindp5  41727  zdivgd  42324  fsuppind  42545  dfac21  43023  eexinst11  44498  ax6e2eq  44528  e222  44607  e111  44645  e333  44704  natlocalincr  46795  tworepnotupword  46805  imarnf1pr  47197  2ffzoeq  47242  iccpartigtl  47297  iccpartgt  47301  lighneallem3  47481  lighneal  47485  requad1  47496  evenltle  47591  fppr2odd  47605  sgoldbeven3prm  47657  bgoldbtbndlem2  47680  lincdifsn  48153  lindslinindimp2lem4  48190  snlindsntor  48200  lincresunit3lem1  48208  lincresunit3lem2  48209  f002  48567  setrec1lem2  48780