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  1995  axc16i  2465  eupickbi  2661  ceqsalgALT  3486  cgsexg  3494  cgsex2g  3495  cgsex4g  3496  spcegv  3551  spc2egv  3553  disjne  4407  uneqdifeq  4447  preqsnd  4813  preq12nebg  4817  opthprneg  4819  dfiun2g  4987  axprlem4  5387  pocl  5566  relresfldOLD  6279  unixpid  6287  ordnbtwn  6458  sucssel  6460  ordelinel  6466  funmo  6555  fvimacnv  7053  ordsuc  7826  tfi  7865  focdmex  7969  f1ovv  7971  opreuopreu  8047  frrlem4  8311  tz7.49  8459  oeworde  8606  fsetprcnex  8888  dom2d  9024  findcard  9183  fisupg  9283  dffi3  9427  noinfep  9665  cantnflem2  9695  ttrcltr  9721  tcmin  9744  rankr1ag  9814  rankunb  9868  rankxpsuc  9903  setrec1lem2  9971  alephordi  10157  alephsucdom  10162  alephinit  10178  dfac9  10219  ackbij2lem4  10323  cff1  10340  cfslbn  10349  cfcoflem  10354  cfcof  10356  infpssrlem5  10389  isfin7-2  10478  acncc  10522  domtriomlem  10524  axdc3lem2  10533  ttukeylem1  10591  iundom2g  10628  axpowndlem3  10688  wunex2  10827  grupr  10886  gruiun  10888  eltskm  10932  nqereu  11018  addcanpr  11135  axpre-sup  11258  relin01  11844  nneo  12787  zeo2  12790  xrub  13446  uznfz  13748  difelfzle  13779  ssfzo12  13898  facndiv  14436  hashgt12el2  14572  hash2prde  14619  hash2pwpr  14625  hashle2prv  14627  tpfo  14649  fi1uzind  14656  swrdswrd  14859  pfxccatin12lem2  14885  pfxccatin12  14887  pfxccat3  14888  cshwidxmod  14959  2cshwcshw  14981  fsumcom2  15946  fprodss  16121  fprodcom2  16157  ndvdssub  16585  eucalglt  16766  prmind2  16866  coprm  16893  prmdiveq  16969  prmdvdsprmop  17227  prmgaplem5  17239  cicsym  17985  drsdir  18482  lublecllem  18538  istos  18596  tsrlin  18765  dirge  18783  mhmlin  18994  issubg2  19358  nsgbi  19373  symgextf1lem  19640  sylow2a  19839  gsumpr  20175  0ringnnzr  20782  0ring01eq  20786  01eq0ringOLD  20788  nrhmzr  20795  issubrng2  20816  issubrg2  20850  isdrng5  21014  abvmul  21084  abvtri  21085  lmodlema  21146  rmodislmodlem  21210  rmodislmod  21211  ellspsn6  21275  lmhmlin  21316  lbsind  21361  isprmidlc  21634  nzerooringczr  21792  ipcj  21946  obsip  22033  lindsss  22136  mamufacex  22717  mavmulsolcl  22872  slesolvec  23003  inopn  23223  basis1  23274  tgss  23292  tgcl  23293  elcls3  23407  neindisj2  23447  cncls  23598  1stcelcls  23786  qtoptop2  24024  nrmr0reg  24074  fbasssin  24161  fbfinnfr  24166  fbunfip  24194  filufint  24245  uffix  24246  ufinffr  24254  ufilen  24255  fmfnfmlem1  24279  flftg  24321  alexsubALT  24376  xmeteq0  24663  blssexps  24751  blssex  24752  mopni3  24819  neibl  24826  metss  24833  metcnp3  24865  nmvs  25001  iccntr  25147  reconnlem2  25153  lebnumlem3  25290  caubl  25635  bcthlem5  25655  ovolunlem1  25824  voliunlem1  25877  volsuplem  25882  ellimc3  26205  logbgcd1irr  27128  lgsqrmodndvds  27686  gausslemma2dlem0i  27697  2lgsoddprmlem3  27747  dchrisumlema  27821  nofv  28020  nolesgn2o  28034  nogesgn1o  28036  nosupbnd1lem5  28075  addsprop  28368  negsprop  28427  mulsprop  28522  precsexlem6  28604  precsexlem7  28605  umgrnloopv  29690  usgrnloopvALT  29788  umgrres1lem  29897  upgrres1  29900  nbuhgr  29930  cplgrop  30024  fusgrregdegfi  30156  g0wlk0  30237  wlkdlem2  30268  upgrwlkdvdelem  30328  crctcshwlkn0lem3  30407  crctcshwlkn0lem5  30409  wspn0  30519  usgrwwlks2on  30553  umgrwwlks2on  30554  elwspths2spth  30565  clwlkclwwlklem2a  30595  clwlkclwwlklem3  30598  clwwlkn1loopb  30640  clwwlknonwwlknonb  30703  clwwlknonex2lem2  30705  3cyclfrgrrn2  30894  frgrncvvdeqlem8  30913  frgrwopregasn  30923  frgrwopregbsn  30924  frgrwopreg1  30925  frgrwopreg2  30926  frgrregord013  31002  frgrogt3nreg  31004  ablocom  31156  ubthlem1  31478  shaddcl  31825  shmulcl  31826  spansnss2  32183  cnopc  32521  cnfnc  32538  adj1  32541  pjorthcoi  32777  stj  32843  mdsl1i  32929  chirredlem1  32998  mdsymlem5  33015  cdj3lem2b  33045  slmdlema  33811  soinfdom  35769  acwer1prc  35817  vonf1oonfo  35969  pconncn  36076  cvmlift2lem1  36154  fmla0xp  36235  ss2mcls  36420  antnestlaw2  36544  dfon2lem6  36643  waj-ax  37295  lukshef-ax2  37296  tr0elw  37365  bj-alrim  37688  bj-nexdt  37692  sucneqond  38382  rdgssun  38395  ptrecube  38632  poimirlem26  38658  poimirlem29  38661  heiborlem1  38839  rngodm1dm2  38960  rngoueqz  38968  zerdivemp1x  38975  isdrngo3  38987  0rngo  39055  pridl  39065  ispridlc  39098  isdmn3  39102  dmnnzd  39103  elrelscnveq3  39653  lshpcmp  40139  omllaw  40394  dochexmidlem7  42617  lspindp5  42921  zdivgd  43482  fsuppind  43712  dfac21  44162  eexinst11  45604  ax6e2eq  45634  e222  45713  e111  45751  e333  45809  imarnf1pr  48446  2ffzoeq  48492  iccpartigtl  48599  iccpartgt  48603  lighneallem3  48786  lighneal  48790  requad1  48814  evenltle  48909  fppr2odd  48923  sgoldbeven3prm  48975  bgoldbtbndlem2  48998  isubgr3stgrlem4  49161  isubgr3stgrlem7  49164  gpgedg2iv  49259  isidom3  49536  idomnzd  49537  lincdifsn  49630  lindslinindimp2lem4  49667  snlindsntor  49677  lincresunit3lem1  49685  lincresunit3lem2  49686  f002  50059