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  1964  axc16i  2440  eupickbi  2636  ceqsalgALT  3477  cgsexg  3485  cgsex2g  3486  cgsex4g  3487  cgsex4gOLD  3488  spcegv  3551  spc2egv  3553  disjne  4407  uneqdifeq  4445  preqsnd  4815  preq12nebg  4819  opthprneg  4821  dfiun2g  4985  axprlem4  5371  pocl  5540  relresfld  6234  unixpid  6242  ordnbtwn  6412  sucssel  6414  ordelinel  6420  funmo  6508  fvimacnv  6998  ordsuc  7756  tfi  7795  focdmex  7900  f1ovv  7902  opreuopreu  7978  frrlem4  8231  tz7.49  8376  oeworde  8521  fsetprcnex  8799  dom2d  8930  findcard  9088  fisupg  9188  dffi3  9334  noinfep  9569  cantnflem2  9599  ttrcltr  9625  tcmin  9648  rankr1ag  9714  rankunb  9762  rankxpsuc  9794  alephordi  9984  alephsucdom  9989  alephinit  10005  dfac9  10047  ackbij2lem4  10151  cff1  10168  cfslbn  10177  cfcoflem  10182  cfcof  10184  infpssrlem5  10217  isfin7-2  10306  acncc  10350  domtriomlem  10352  axdc3lem2  10361  ttukeylem1  10419  iundom2g  10450  axpowndlem3  10510  wunex2  10649  grupr  10708  gruiun  10710  eltskm  10754  nqereu  10840  addcanpr  10957  axpre-sup  11080  relin01  11661  nneo  12576  zeo2  12579  xrub  13227  uznfz  13526  difelfzle  13557  ssfzo12  13675  facndiv  14211  hashgt12el2  14346  hash2prde  14393  hash2pwpr  14399  hashle2prv  14401  tpfo  14423  fi1uzind  14430  swrdswrd  14628  pfxccatin12lem2  14654  pfxccatin12  14656  pfxccat3  14657  cshwidxmod  14726  2cshwcshw  14748  fsumcom2  15697  fprodss  15871  fprodcom2  15907  sumodd  16315  ndvdssub  16336  eucalglt  16512  prmind2  16612  coprm  16638  prmdiveq  16713  prmdvdsprmop  16971  prmgaplem5  16983  cicsym  17728  drsdir  18225  lublecllem  18281  istos  18339  tsrlin  18508  dirge  18526  mhmlin  18718  issubg2  19071  nsgbi  19086  symgextf1lem  19349  sylow2a  19548  gsumpr  19884  0ringnnzr  20458  0ring01eq  20462  01eq0ringOLD  20464  nrhmzr  20470  issubrng2  20491  issubrg2  20525  abvmul  20754  abvtri  20755  lmodlema  20816  rmodislmodlem  20880  rmodislmod  20881  ellspsn6  20945  lmhmlin  20987  lbsind  21032  nzerooringczr  21435  ipcj  21589  obsip  21676  lindsss  21779  mamufacex  22340  mavmulsolcl  22495  slesolvec  22623  inopn  22843  basis1  22894  tgss  22912  tgcl  22913  elcls3  23027  neindisj2  23067  cncls  23218  1stcelcls  23405  qtoptop2  23643  nrmr0reg  23693  fbasssin  23780  fbfinnfr  23785  fbunfip  23813  filufint  23864  uffix  23865  ufinffr  23873  ufilen  23874  fmfnfmlem1  23898  flftg  23940  alexsubALT  23995  xmeteq0  24282  blssexps  24370  blssex  24371  mopni3  24438  neibl  24445  metss  24452  metcnp3  24484  nmvs  24620  iccntr  24766  reconnlem2  24772  lebnumlem3  24918  caubl  25264  bcthlem5  25284  ovolunlem1  25454  voliunlem1  25507  volsuplem  25512  ellimc3  25836  logbgcd1irr  26760  lgsqrmodndvds  27320  gausslemma2dlem0i  27331  2lgsoddprmlem3  27381  dchrisumlema  27455  nofv  27625  nolesgn2o  27639  nogesgn1o  27641  nosupbnd1lem5  27680  addsprop  27972  negsprop  28031  mulsprop  28126  precsexlem6  28208  precsexlem7  28209  umgrnloopv  29179  usgrnloopvALT  29274  umgrres1lem  29383  upgrres1  29386  nbuhgr  29416  cplgrop  29510  fusgrregdegfi  29643  g0wlk0  29724  wlkdlem2  29755  upgrwlkdvdelem  29809  crctcshwlkn0lem3  29885  crctcshwlkn0lem5  29887  wspn0  29997  usgrwwlks2on  30031  umgrwwlks2on  30032  elwspths2spth  30043  clwlkclwwlklem2a  30073  clwlkclwwlklem3  30076  clwwlkn1loopb  30118  clwwlknonwwlknonb  30181  clwwlknonex2lem2  30183  3cyclfrgrrn2  30362  frgrncvvdeqlem8  30381  frgrwopregasn  30391  frgrwopregbsn  30392  frgrwopreg1  30393  frgrwopreg2  30394  frgrregord013  30470  frgrogt3nreg  30472  ablocom  30623  ubthlem1  30945  shaddcl  31292  shmulcl  31293  spansnss2  31650  cnopc  31988  cnfnc  32005  adj1  32008  pjorthcoi  32244  stj  32310  mdsl1i  32396  chirredlem1  32465  mdsymlem5  32482  cdj3lem2b  32512  slmdlema  33285  isprmidlc  33528  pconncn  35418  cvmlift2lem1  35496  fmla0xp  35577  ss2mcls  35762  antnestlaw2  35886  dfon2lem6  35980  waj-ax  36608  lukshef-ax2  36609  bj-alrim  36894  bj-nexdt  36898  sucneqond  37566  rdgssun  37579  ptrecube  37817  poimirlem26  37843  poimirlem29  37846  heiborlem1  38008  rngodm1dm2  38129  rngoueqz  38137  zerdivemp1x  38144  isdrngo3  38156  0rngo  38224  pridl  38234  ispridlc  38267  isdmn3  38271  dmnnzd  38272  elrelscnveq3  38796  lshpcmp  39244  omllaw  39499  dochexmidlem7  41722  lspindp5  42026  zdivgd  42588  fsuppind  42829  dfac21  43304  eexinst11  44764  ax6e2eq  44794  e222  44873  e111  44911  e333  44969  natlocalincr  47116  imarnf1pr  47524  2ffzoeq  47569  iccpartigtl  47665  iccpartgt  47669  lighneallem3  47849  lighneal  47853  requad1  47864  evenltle  47959  fppr2odd  47973  sgoldbeven3prm  48025  bgoldbtbndlem2  48048  isubgr3stgrlem4  48211  isubgr3stgrlem7  48214  gpgedg2iv  48309  lincdifsn  48666  lindslinindimp2lem4  48703  snlindsntor  48713  lincresunit3lem1  48721  lincresunit3lem2  48722  f002  49095  setrec1lem2  49929