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  1998  axc16i  2468  eupickbi  2664  ceqsalgALT  3490  cgsexg  3498  cgsex2g  3499  cgsex4g  3500  spcegv  3555  spc2egv  3557  disjne  4411  uneqdifeq  4451  preqsnd  4819  preq12nebg  4823  opthprneg  4825  dfiun2g  4993  axprlem4  5395  pocl  5574  relresfldOLD  6303  unixpid  6311  ordnbtwn  6484  sucssel  6486  ordelinel  6492  funmo  6582  fvimacnv  7083  ordsuc  7859  tfi  7898  focdmex  8002  f1ovv  8004  opreuopreu  8080  frrlem4  8345  tz7.49  8493  oeworde  8640  fsetprcnex  8922  dom2d  9058  findcard  9217  fisupg  9317  dffi3  9460  noinfep  9698  cantnflem2  9728  ttrcltr  9754  tcmin  9777  rankr1ag  9847  rankunb  9901  rankxpsuc  9936  setrec1lem2  10004  alephordi  10192  alephsucdom  10197  alephinit  10213  dfac9  10254  ackbij2lem4  10358  cff1  10375  cfslbn  10384  cfcoflem  10389  cfcof  10391  infpssrlem5  10424  isfin7-2  10513  acncc  10557  domtriomlem  10559  axdc3lem2  10568  ttukeylem1  10626  iundom2g  10663  axpowndlem3  10723  wunex2  10862  grupr  10921  gruiun  10923  eltskm  10967  nqereu  11053  addcanpr  11170  axpre-sup  11293  relin01  11880  nneo  12823  zeo2  12826  xrub  13482  uznfz  13784  difelfzle  13815  ssfzo12  13934  facndiv  14473  hashgt12el2  14609  hash2prde  14656  hash2pwpr  14662  hashle2prv  14664  tpfo  14686  fi1uzind  14693  swrdswrd  14896  pfxccatin12lem2  14922  pfxccatin12  14924  pfxccat3  14925  cshwidxmod  14996  2cshwcshw  15018  fsumcom2  15984  fprodss  16159  fprodcom2  16195  ndvdssub  16623  eucalglt  16804  prmind2  16904  coprm  16931  prmdiveq  17007  prmdvdsprmop  17265  prmgaplem5  17277  cicsym  18029  drsdir  18526  lublecllem  18582  istos  18640  tsrlin  18809  dirge  18827  mhmlin  19038  issubg2  19402  nsgbi  19417  symgextf1lem  19685  sylow2a  19884  gsumpr  20220  0ringnnzr  20827  0ring01eq  20831  01eq0ringOLD  20833  nrhmzr  20840  issubrng2  20861  issubrg2  20895  isdrng5  21059  abvmul  21129  abvtri  21130  lmodlema  21191  rmodislmodlem  21255  rmodislmod  21256  ellspsn6  21320  lmhmlin  21361  lbsind  21406  isprmidlc  21679  nzerooringczr  21841  ipcj  21995  obsip  22082  lindsss  22185  mamufacex  22766  mavmulsolcl  22921  slesolvec  23052  inopn  23272  basis1  23323  tgss  23341  tgcl  23342  elcls3  23456  neindisj2  23496  cncls  23647  1stcelcls  23835  qtoptop2  24073  nrmr0reg  24123  fbasssin  24210  fbfinnfr  24215  fbunfip  24243  filufint  24294  uffix  24295  ufinffr  24303  ufilen  24304  fmfnfmlem1  24328  flftg  24370  alexsubALT  24425  xmeteq0  24712  blssexps  24800  blssex  24801  mopni3  24868  neibl  24875  metss  24882  metcnp3  24914  nmvs  25050  iccntr  25196  reconnlem2  25202  lebnumlem3  25339  caubl  25684  bcthlem5  25704  ovolunlem1  25873  voliunlem1  25926  volsuplem  25931  ellimc3  26254  logbgcd1irr  27179  lgsqrmodndvds  27737  gausslemma2dlem0i  27748  2lgsoddprmlem3  27798  dchrisumlema  27872  nofv  28071  nolesgn2o  28085  nogesgn1o  28087  nosupbnd1lem5  28126  addsprop  28419  negsprop  28478  mulsprop  28573  precsexlem6  28655  precsexlem7  28656  umgrnloopv  29741  usgrnloopvALT  29839  umgrres1lem  29948  upgrres1  29951  nbuhgr  29981  cplgrop  30075  fusgrregdegfi  30207  g0wlk0  30288  wlkdlem2  30319  upgrwlkdvdelem  30379  crctcshwlkn0lem3  30458  crctcshwlkn0lem5  30460  wspn0  30570  usgrwwlks2on  30604  umgrwwlks2on  30605  elwspths2spth  30616  clwlkclwwlklem2a  30646  clwlkclwwlklem3  30649  clwwlkn1loopb  30691  clwwlknonwwlknonb  30754  clwwlknonex2lem2  30756  3cyclfrgrrn2  30945  frgrncvvdeqlem8  30964  frgrwopregasn  30974  frgrwopregbsn  30975  frgrwopreg1  30976  frgrwopreg2  30977  frgrregord013  31053  frgrogt3nreg  31055  ablocom  31207  ubthlem1  31529  shaddcl  31876  shmulcl  31877  spansnss2  32234  cnopc  32572  cnfnc  32589  adj1  32592  pjorthcoi  32828  stj  32894  mdsl1i  32980  chirredlem1  33049  mdsymlem5  33066  cdj3lem2b  33096  slmdlema  33863  soinfdom  35841  acwer1prc  35893  vonf1oonfo  36090  pconncn  36197  cvmlift2lem1  36275  fmla0xp  36356  ss2mcls  36541  antnestlaw2  36665  dfon2lem6  36765  waj-ax  37417  lukshef-ax2  37418  tr0elw  37487  bj-alrim  37810  bj-nexdt  37814  sucneqond  38556  rdgssun  38569  ptrecube  38806  poimirlem26  38832  poimirlem29  38835  heiborlem1  39011  rngodm1dm2  39132  rngoueqz  39140  zerdivemp1x  39147  isdrngo3  39159  0rngo  39227  pridl  39237  ispridlc  39270  isdmn3  39274  dmnnzd  39275  elrelscnveq3  39825  lshpcmp  40311  omllaw  40566  dochexmidlem7  42789  lspindp5  43093  zdivgd  43654  fsuppind  43884  dfac21  44334  eexinst11  45770  ax6e2eq  45800  e222  45879  e111  45917  e333  45975  imarnf1pr  48625  2ffzoeq  48671  iccpartigtl  48778  iccpartgt  48782  lighneallem3  48965  lighneal  48969  requad1  48993  evenltle  49088  fppr2odd  49102  sgoldbeven3prm  49154  bgoldbtbndlem2  49177  isubgr3stgrlem4  49340  isubgr3stgrlem7  49343  gpgedg2iv  49438  isidom3  49773  idomnzd  49774  lincdifsn  49867  lindslinindimp2lem4  49904  snlindsntor  49914  lincresunit3lem1  49922  lincresunit3lem2  49923  f002  50296