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  1970  axc16i  2444  eupickbi  2640  ceqsalgALT  3469  cgsexg  3477  cgsex2g  3478  cgsex4g  3479  spcegv  3542  spc2egv  3544  disjne  4390  uneqdifeq  4427  preqsnd  4797  preq12nebg  4801  opthprneg  4803  dfiun2g  4966  axprlem4  5362  pocl  5541  relresfld  6234  unixpid  6242  ordnbtwn  6412  sucssel  6414  ordelinel  6420  funmo  6508  fvimacnv  7001  ordsuc  7761  tfi  7800  focdmex  7905  f1ovv  7907  opreuopreu  7983  frrlem4  8236  tz7.49  8381  oeworde  8526  fsetprcnex  8806  dom2d  8937  findcard  9095  fisupg  9195  dffi3  9341  noinfep  9579  cantnflem2  9609  ttrcltr  9635  tcmin  9658  rankr1ag  9724  rankunb  9772  rankxpsuc  9804  alephordi  9994  alephsucdom  9999  alephinit  10015  dfac9  10057  ackbij2lem4  10161  cff1  10178  cfslbn  10187  cfcoflem  10192  cfcof  10194  infpssrlem5  10227  isfin7-2  10316  acncc  10360  domtriomlem  10362  axdc3lem2  10371  ttukeylem1  10429  iundom2g  10460  axpowndlem3  10520  wunex2  10659  grupr  10718  gruiun  10720  eltskm  10764  nqereu  10850  addcanpr  10967  axpre-sup  11090  relin01  11672  nneo  12611  zeo2  12614  xrub  13262  uznfz  13562  difelfzle  13593  ssfzo12  13712  facndiv  14248  hashgt12el2  14383  hash2prde  14430  hash2pwpr  14436  hashle2prv  14438  tpfo  14460  fi1uzind  14467  swrdswrd  14665  pfxccatin12lem2  14691  pfxccatin12  14693  pfxccat3  14694  cshwidxmod  14763  2cshwcshw  14785  fsumcom2  15734  fprodss  15911  fprodcom2  15947  sumodd  16355  ndvdssub  16376  eucalglt  16552  prmind2  16652  coprm  16679  prmdiveq  16754  prmdvdsprmop  17012  prmgaplem5  17024  cicsym  17769  drsdir  18266  lublecllem  18322  istos  18380  tsrlin  18549  dirge  18567  mhmlin  18759  issubg2  19115  nsgbi  19130  symgextf1lem  19393  sylow2a  19592  gsumpr  19928  0ringnnzr  20504  0ring01eq  20508  01eq0ringOLD  20510  nrhmzr  20516  issubrng2  20537  issubrg2  20571  abvmul  20800  abvtri  20801  lmodlema  20862  rmodislmodlem  20926  rmodislmod  20927  ellspsn6  20991  lmhmlin  21032  lbsind  21077  nzerooringczr  21462  ipcj  21616  obsip  21703  lindsss  21806  mamufacex  22386  mavmulsolcl  22541  slesolvec  22669  inopn  22889  basis1  22940  tgss  22958  tgcl  22959  elcls3  23073  neindisj2  23113  cncls  23264  1stcelcls  23451  qtoptop2  23689  nrmr0reg  23739  fbasssin  23826  fbfinnfr  23831  fbunfip  23859  filufint  23910  uffix  23911  ufinffr  23919  ufilen  23920  fmfnfmlem1  23944  flftg  23986  alexsubALT  24041  xmeteq0  24328  blssexps  24416  blssex  24417  mopni3  24484  neibl  24491  metss  24498  metcnp3  24530  nmvs  24666  iccntr  24812  reconnlem2  24818  lebnumlem3  24955  caubl  25300  bcthlem5  25320  ovolunlem1  25489  voliunlem1  25542  volsuplem  25547  ellimc3  25871  logbgcd1irr  26783  lgsqrmodndvds  27341  gausslemma2dlem0i  27352  2lgsoddprmlem3  27402  dchrisumlema  27476  nofv  27646  nolesgn2o  27660  nogesgn1o  27662  nosupbnd1lem5  27701  addsprop  27993  negsprop  28052  mulsprop  28147  precsexlem6  28229  precsexlem7  28230  umgrnloopv  29200  usgrnloopvALT  29295  umgrres1lem  29404  upgrres1  29407  nbuhgr  29437  cplgrop  29531  fusgrregdegfi  29663  g0wlk0  29744  wlkdlem2  29775  upgrwlkdvdelem  29829  crctcshwlkn0lem3  29905  crctcshwlkn0lem5  29907  wspn0  30017  usgrwwlks2on  30051  umgrwwlks2on  30052  elwspths2spth  30063  clwlkclwwlklem2a  30093  clwlkclwwlklem3  30096  clwwlkn1loopb  30138  clwwlknonwwlknonb  30201  clwwlknonex2lem2  30203  3cyclfrgrrn2  30382  frgrncvvdeqlem8  30401  frgrwopregasn  30411  frgrwopregbsn  30412  frgrwopreg1  30413  frgrwopreg2  30414  frgrregord013  30490  frgrogt3nreg  30492  ablocom  30644  ubthlem1  30966  shaddcl  31313  shmulcl  31314  spansnss2  31671  cnopc  32009  cnfnc  32026  adj1  32029  pjorthcoi  32265  stj  32331  mdsl1i  32417  chirredlem1  32486  mdsymlem5  32503  cdj3lem2b  32533  slmdlema  33291  isprmidlc  33537  pconncn  35459  cvmlift2lem1  35537  fmla0xp  35618  ss2mcls  35803  antnestlaw2  35927  dfon2lem6  36021  waj-ax  36649  lukshef-ax2  36650  tr0elw  36719  bj-alrim  37043  bj-nexdt  37047  sucneqond  37734  rdgssun  37747  ptrecube  37994  poimirlem26  38020  poimirlem29  38023  heiborlem1  38185  rngodm1dm2  38306  rngoueqz  38314  zerdivemp1x  38321  isdrngo3  38333  0rngo  38401  pridl  38411  ispridlc  38444  isdmn3  38448  dmnnzd  38449  elrelscnveq3  39001  lshpcmp  39487  omllaw  39742  dochexmidlem7  41965  lspindp5  42269  zdivgd  42821  fsuppind  43047  dfac21  43518  eexinst11  44978  ax6e2eq  45008  e222  45087  e111  45125  e333  45183  natlocalincr  47328  imarnf1pr  47752  2ffzoeq  47798  iccpartigtl  47905  iccpartgt  47909  lighneallem3  48092  lighneal  48096  requad1  48120  evenltle  48215  fppr2odd  48229  sgoldbeven3prm  48281  bgoldbtbndlem2  48304  isubgr3stgrlem4  48467  isubgr3stgrlem7  48470  gpgedg2iv  48565  lincdifsn  48922  lindslinindimp2lem4  48959  snlindsntor  48969  lincresunit3lem1  48977  lincresunit3lem2  48978  f002  49351  setrec1lem2  50185