Theorem syl5com 32

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 26	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
3		syl5com.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	sylcom 31	1 ⊢ (𝜑 → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com12  33  syl5  35  speimfw  1996  axc16i  2471  eupickbi  2667  ceqsalgALT  3494  cgsexg  3502  cgsex2g  3503  cgsex4g  3504  spcegv  3559  spc2egv  3561  disjne  4418  uneqdifeq  4458  preqsnd  4829  preq12nebg  4833  opthprneg  4835  dfiun2g  4999  axprlem4  5402  pocl  5582  relresfldOLD  6284  unixpid  6292  ordnbtwn  6463  sucssel  6465  ordelinel  6471  funmo  6559  fvimacnv  7055  ordsuc  7819  tfi  7858  focdmex  7962  f1ovv  7964  opreuopreu  8040  frrlem4  8295  tz7.49  8441  oeworde  8588  fsetprcnex  8868  dom2d  8999  findcard  9158  fisupg  9258  dffi3  9401  noinfep  9639  cantnflem2  9669  ttrcltr  9695  tcmin  9718  rankr1ag  9784  rankunb  9832  rankxpsuc  9864  alephordi  10077  alephsucdom  10082  alephinit  10098  dfac9  10139  ackbij2lem4  10243  cff1  10260  cfslbn  10269  cfcoflem  10274  cfcof  10276  infpssrlem5  10309  isfin7-2  10398  acncc  10442  domtriomlem  10444  axdc3lem2  10453  ttukeylem1  10511  iundom2g  10542  axpowndlem3  10602  wunex2  10741  grupr  10800  gruiun  10802  eltskm  10846  nqereu  10932  addcanpr  11049  axpre-sup  11172  relin01  11756  nneo  12698  zeo2  12701  xrub  13356  uznfz  13657  difelfzle  13688  ssfzo12  13807  facndiv  14344  hashgt12el2  14480  hash2prde  14527  hash2pwpr  14533  hashle2prv  14535  tpfo  14557  fi1uzind  14564  swrdswrd  14766  pfxccatin12lem2  14792  pfxccatin12  14794  pfxccat3  14795  cshwidxmod  14866  2cshwcshw  14888  fsumcom2  15851  fprodss  16028  fprodcom2  16064  ndvdssub  16492  eucalglt  16668  prmind2  16768  coprm  16795  prmdiveq  16870  prmdvdsprmop  17128  prmgaplem5  17140  cicsym  17886  drsdir  18383  lublecllem  18439  istos  18497  tsrlin  18666  dirge  18684  mhmlin  18882  issubg2  19239  nsgbi  19254  symgextf1lem  19521  sylow2a  19720  gsumpr  20056  0ringnnzr  20660  0ring01eq  20664  01eq0ringOLD  20666  nrhmzr  20673  issubrng2  20694  issubrg2  20728  isdrng5  20891  abvmul  20961  abvtri  20962  lmodlema  21023  rmodislmodlem  21087  rmodislmod  21088  ellspsn6  21152  lmhmlin  21193  lbsind  21238  isprmidlc  21509  nzerooringczr  21667  ipcj  21821  obsip  21908  lindsss  22011  mamufacex  22590  mavmulsolcl  22745  slesolvec  22873  inopn  23093  basis1  23144  tgss  23162  tgcl  23163  elcls3  23277  neindisj2  23317  cncls  23468  1stcelcls  23655  qtoptop2  23893  nrmr0reg  23943  fbasssin  24030  fbfinnfr  24035  fbunfip  24063  filufint  24114  uffix  24115  ufinffr  24123  ufilen  24124  fmfnfmlem1  24148  flftg  24190  alexsubALT  24245  xmeteq0  24532  blssexps  24620  blssex  24621  mopni3  24688  neibl  24695  metss  24702  metcnp3  24734  nmvs  24870  iccntr  25016  reconnlem2  25022  lebnumlem3  25159  caubl  25504  bcthlem5  25524  ovolunlem1  25693  voliunlem1  25746  volsuplem  25751  ellimc3  26075  logbgcd1irr  26996  lgsqrmodndvds  27554  gausslemma2dlem0i  27565  2lgsoddprmlem3  27615  dchrisumlema  27689  nofv  27858  nolesgn2o  27872  nogesgn1o  27874  nosupbnd1lem5  27913  addsprop  28206  negsprop  28265  mulsprop  28360  precsexlem6  28442  precsexlem7  28443  umgrnloopv  29493  usgrnloopvALT  29588  umgrres1lem  29697  upgrres1  29700  nbuhgr  29730  cplgrop  29824  fusgrregdegfi  29956  g0wlk0  30037  wlkdlem2  30068  upgrwlkdvdelem  30122  crctcshwlkn0lem3  30198  crctcshwlkn0lem5  30200  wspn0  30310  usgrwwlks2on  30344  umgrwwlks2on  30345  elwspths2spth  30356  clwlkclwwlklem2a  30386  clwlkclwwlklem3  30389  clwwlkn1loopb  30431  clwwlknonwwlknonb  30494  clwwlknonex2lem2  30496  3cyclfrgrrn2  30675  frgrncvvdeqlem8  30694  frgrwopregasn  30704  frgrwopregbsn  30705  frgrwopreg1  30706  frgrwopreg2  30707  frgrregord013  30783  frgrogt3nreg  30785  ablocom  30937  ubthlem1  31259  shaddcl  31606  shmulcl  31607  spansnss2  31964  cnopc  32302  cnfnc  32319  adj1  32322  pjorthcoi  32558  stj  32624  mdsl1i  32710  chirredlem1  32779  mdsymlem5  32796  cdj3lem2b  32826  slmdlema  33554  vonf1oonfo  35623  pconncn  35737  cvmlift2lem1  35815  fmla0xp  35896  ss2mcls  36081  antnestlaw2  36205  dfon2lem6  36299  waj-ax  36966  lukshef-ax2  36967  tr0elw  37036  bj-alrim  37359  bj-nexdt  37363  sucneqond  38052  rdgssun  38065  ptrecube  38312  poimirlem26  38338  poimirlem29  38341  heiborlem1  38503  rngodm1dm2  38624  rngoueqz  38632  zerdivemp1x  38639  isdrngo3  38651  0rngo  38719  pridl  38729  ispridlc  38762  isdmn3  38766  dmnnzd  38767  elrelscnveq3  39317  lshpcmp  39803  omllaw  40058  dochexmidlem7  42281  lspindp5  42585  zdivgd  43139  fsuppind  43363  dfac21  43834  eexinst11  45277  ax6e2eq  45307  e222  45386  e111  45424  e333  45482  natlocalincr  47633  imarnf1pr  48060  2ffzoeq  48106  iccpartigtl  48213  iccpartgt  48217  lighneallem3  48400  lighneal  48404  requad1  48428  evenltle  48523  fppr2odd  48537  sgoldbeven3prm  48589  bgoldbtbndlem2  48612  isubgr3stgrlem4  48775  isubgr3stgrlem7  48778  gpgedg2iv  48873  isidom3  49151  idomnzd  49152  lincdifsn  49245  lindslinindimp2lem4  49282  snlindsntor  49292  lincresunit3lem1  49300  lincresunit3lem2  49301  f002  49673  setrec1lem2  50507