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  2440  eupickbi  2635  ceqsalgALT  3497  cgsexg  3505  cgsex2g  3506  cgsex4g  3507  cgsex4gOLD  3508  spcegv  3576  spc2egv  3578  disjne  4430  uneqdifeq  4468  preqsnd  4835  preq12nebg  4839  opthprneg  4841  dfiun2g  5006  axprlem4  5396  pocl  5569  relresfld  6265  unixpid  6273  ordnbtwn  6446  sucssel  6448  ordelinel  6454  funmo  6550  fvimacnv  7042  ordsuc  7805  ordsucOLD  7806  tfi  7846  focdmex  7952  f1ovv  7954  opreuopreu  8031  frrlem4  8286  wfrlem4OLD  8324  wfrlem10OLD  8330  tz7.49  8457  oeworde  8603  fsetprcnex  8874  dom2d  9005  findcard  9175  fisupg  9294  dffi3  9441  noinfep  9672  cantnflem2  9702  ttrcltr  9728  tcmin  9753  rankr1ag  9814  rankunb  9862  rankxpsuc  9894  alephordi  10086  alephsucdom  10091  alephinit  10107  dfac9  10149  ackbij2lem4  10253  cff1  10270  cfslbn  10279  cfcoflem  10284  cfcof  10286  infpssrlem5  10319  isfin7-2  10408  acncc  10452  domtriomlem  10454  axdc3lem2  10463  ttukeylem1  10521  iundom2g  10552  axpowndlem3  10611  wunex2  10750  grupr  10809  gruiun  10811  eltskm  10855  nqereu  10941  addcanpr  11058  axpre-sup  11181  relin01  11759  nneo  12675  zeo2  12678  xrub  13326  uznfz  13625  difelfzle  13656  ssfzo12  13773  facndiv  14304  hashgt12el2  14439  hash2prde  14486  hash2pwpr  14492  hashle2prv  14494  tpfo  14516  fi1uzind  14523  swrdswrd  14721  pfxccatin12lem2  14747  pfxccatin12  14749  pfxccat3  14750  cshwidxmod  14819  2cshwcshw  14842  fsumcom2  15788  fprodss  15962  fprodcom2  15998  sumodd  16405  ndvdssub  16426  eucalglt  16602  prmind2  16702  coprm  16728  prmdiveq  16803  prmdvdsprmop  17061  prmgaplem5  17073  cicsym  17815  drsdir  18312  lublecllem  18368  istos  18426  tsrlin  18593  dirge  18611  mhmlin  18769  issubg2  19122  nsgbi  19138  symgextf1lem  19399  sylow2a  19598  gsumpr  19934  0ringnnzr  20483  0ring01eq  20487  01eq0ringOLD  20489  nrhmzr  20495  issubrng2  20516  issubrg2  20550  abvmul  20779  abvtri  20780  lmodlema  20820  rmodislmodlem  20884  rmodislmod  20885  ellspsn6  20949  lmhmlin  20991  lbsind  21036  nzerooringczr  21439  ipcj  21592  obsip  21679  lindsss  21782  mamufacex  22332  mavmulsolcl  22487  slesolvec  22615  inopn  22835  basis1  22886  tgss  22904  tgcl  22905  elcls3  23019  neindisj2  23059  cncls  23210  1stcelcls  23397  qtoptop2  23635  nrmr0reg  23685  fbasssin  23772  fbfinnfr  23777  fbunfip  23805  filufint  23856  uffix  23857  ufinffr  23865  ufilen  23866  fmfnfmlem1  23890  flftg  23932  alexsubALT  23987  xmeteq0  24275  blssexps  24363  blssex  24364  mopni3  24431  neibl  24438  metss  24445  metcnp3  24477  nmvs  24613  iccntr  24759  reconnlem2  24765  lebnumlem3  24911  caubl  25258  bcthlem5  25278  ovolunlem1  25448  voliunlem1  25501  volsuplem  25506  ellimc3  25830  logbgcd1irr  26754  lgsqrmodndvds  27314  gausslemma2dlem0i  27325  2lgsoddprmlem3  27375  dchrisumlema  27449  nofv  27619  nolesgn2o  27633  nogesgn1o  27635  nosupbnd1lem5  27674  addsprop  27926  negsprop  27984  mulsprop  28073  precsexlem6  28153  precsexlem7  28154  umgrnloopv  29031  usgrnloopvALT  29126  umgrres1lem  29235  upgrres1  29238  nbuhgr  29268  cplgrop  29362  fusgrregdegfi  29495  g0wlk0  29578  wlkdlem2  29609  upgrwlkdvdelem  29664  crctcshwlkn0lem3  29740  crctcshwlkn0lem5  29742  wspn0  29852  umgrwwlks2on  29885  elwspths2spth  29895  clwlkclwwlklem2a  29925  clwlkclwwlklem3  29928  clwwlkn1loopb  29970  clwwlknonwwlknonb  30033  clwwlknonex2lem2  30035  3cyclfrgrrn2  30214  frgrncvvdeqlem8  30233  frgrwopregasn  30243  frgrwopregbsn  30244  frgrwopreg1  30245  frgrwopreg2  30246  frgrregord013  30322  frgrogt3nreg  30324  ablocom  30475  ubthlem1  30797  shaddcl  31144  shmulcl  31145  spansnss2  31502  cnopc  31840  cnfnc  31857  adj1  31860  pjorthcoi  32096  stj  32162  mdsl1i  32248  chirredlem1  32317  mdsymlem5  32334  cdj3lem2b  32364  slmdlema  33146  isprmidlc  33408  pconncn  35192  cvmlift2lem1  35270  fmla0xp  35351  ss2mcls  35536  dfon2lem6  35752  waj-ax  36378  lukshef-ax2  36379  bj-alrim  36657  bj-nexdt  36661  sucneqond  37329  rdgssun  37342  ptrecube  37590  poimirlem26  37616  poimirlem29  37619  heiborlem1  37781  rngodm1dm2  37902  rngoueqz  37910  zerdivemp1x  37917  isdrngo3  37929  0rngo  37997  pridl  38007  ispridlc  38040  isdmn3  38044  dmnnzd  38045  elrelscnveq3  38455  lshpcmp  38952  omllaw  39207  dochexmidlem7  41431  lspindp5  41735  zdivgd  42333  fsuppind  42560  dfac21  43037  eexinst11  44500  ax6e2eq  44530  e222  44609  e111  44647  e333  44705  natlocalincr  46853  tworepnotupword  46863  imarnf1pr  47259  2ffzoeq  47304  iccpartigtl  47385  iccpartgt  47389  lighneallem3  47569  lighneal  47573  requad1  47584  evenltle  47679  fppr2odd  47693  sgoldbeven3prm  47745  bgoldbtbndlem2  47768  isubgr3stgrlem4  47929  isubgr3stgrlem7  47932  lincdifsn  48348  lindslinindimp2lem4  48385  snlindsntor  48395  lincresunit3lem1  48403  lincresunit3lem2  48404  f002  48780  setrec1lem2  49500