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  2436  eupickbi  2631  ceqsalgALT  3473  cgsexg  3481  cgsex2g  3482  cgsex4g  3483  cgsex4gOLD  3484  spcegv  3547  spc2egv  3549  disjne  4404  uneqdifeq  4442  preqsnd  4810  preq12nebg  4814  opthprneg  4816  dfiun2g  4980  axprlem4  5366  pocl  5535  relresfld  6229  unixpid  6237  ordnbtwn  6407  sucssel  6409  ordelinel  6415  funmo  6503  fvimacnv  6992  ordsuc  7750  tfi  7789  focdmex  7894  f1ovv  7896  opreuopreu  7972  frrlem4  8225  tz7.49  8370  oeworde  8514  fsetprcnex  8792  dom2d  8921  findcard  9079  fisupg  9178  dffi3  9321  noinfep  9556  cantnflem2  9586  ttrcltr  9612  tcmin  9635  rankr1ag  9701  rankunb  9749  rankxpsuc  9781  alephordi  9971  alephsucdom  9976  alephinit  9992  dfac9  10034  ackbij2lem4  10138  cff1  10155  cfslbn  10164  cfcoflem  10169  cfcof  10171  infpssrlem5  10204  isfin7-2  10293  acncc  10337  domtriomlem  10339  axdc3lem2  10348  ttukeylem1  10406  iundom2g  10437  axpowndlem3  10496  wunex2  10635  grupr  10694  gruiun  10696  eltskm  10740  nqereu  10826  addcanpr  10943  axpre-sup  11066  relin01  11647  nneo  12563  zeo2  12566  xrub  13217  uznfz  13516  difelfzle  13547  ssfzo12  13665  facndiv  14201  hashgt12el2  14336  hash2prde  14383  hash2pwpr  14389  hashle2prv  14391  tpfo  14413  fi1uzind  14420  swrdswrd  14618  pfxccatin12lem2  14644  pfxccatin12  14646  pfxccat3  14647  cshwidxmod  14716  2cshwcshw  14738  fsumcom2  15687  fprodss  15861  fprodcom2  15897  sumodd  16305  ndvdssub  16326  eucalglt  16502  prmind2  16602  coprm  16628  prmdiveq  16703  prmdvdsprmop  16961  prmgaplem5  16973  cicsym  17717  drsdir  18214  lublecllem  18270  istos  18328  tsrlin  18497  dirge  18515  mhmlin  18707  issubg2  19060  nsgbi  19075  symgextf1lem  19338  sylow2a  19537  gsumpr  19873  0ringnnzr  20446  0ring01eq  20450  01eq0ringOLD  20452  nrhmzr  20458  issubrng2  20479  issubrg2  20513  abvmul  20742  abvtri  20743  lmodlema  20804  rmodislmodlem  20868  rmodislmod  20869  ellspsn6  20933  lmhmlin  20975  lbsind  21020  nzerooringczr  21423  ipcj  21577  obsip  21664  lindsss  21767  mamufacex  22317  mavmulsolcl  22472  slesolvec  22600  inopn  22820  basis1  22871  tgss  22889  tgcl  22890  elcls3  23004  neindisj2  23044  cncls  23195  1stcelcls  23382  qtoptop2  23620  nrmr0reg  23670  fbasssin  23757  fbfinnfr  23762  fbunfip  23790  filufint  23841  uffix  23842  ufinffr  23850  ufilen  23851  fmfnfmlem1  23875  flftg  23917  alexsubALT  23972  xmeteq0  24259  blssexps  24347  blssex  24348  mopni3  24415  neibl  24422  metss  24429  metcnp3  24461  nmvs  24597  iccntr  24743  reconnlem2  24749  lebnumlem3  24895  caubl  25241  bcthlem5  25261  ovolunlem1  25431  voliunlem1  25484  volsuplem  25489  ellimc3  25813  logbgcd1irr  26737  lgsqrmodndvds  27297  gausslemma2dlem0i  27308  2lgsoddprmlem3  27358  dchrisumlema  27432  nofv  27602  nolesgn2o  27616  nogesgn1o  27618  nosupbnd1lem5  27657  addsprop  27925  negsprop  27983  mulsprop  28075  precsexlem6  28156  precsexlem7  28157  umgrnloopv  29091  usgrnloopvALT  29186  umgrres1lem  29295  upgrres1  29298  nbuhgr  29328  cplgrop  29422  fusgrregdegfi  29555  g0wlk0  29636  wlkdlem2  29667  upgrwlkdvdelem  29721  crctcshwlkn0lem3  29797  crctcshwlkn0lem5  29799  wspn0  29909  usgrwwlks2on  29943  umgrwwlks2on  29944  elwspths2spth  29955  clwlkclwwlklem2a  29985  clwlkclwwlklem3  29988  clwwlkn1loopb  30030  clwwlknonwwlknonb  30093  clwwlknonex2lem2  30095  3cyclfrgrrn2  30274  frgrncvvdeqlem8  30293  frgrwopregasn  30303  frgrwopregbsn  30304  frgrwopreg1  30305  frgrwopreg2  30306  frgrregord013  30382  frgrogt3nreg  30384  ablocom  30535  ubthlem1  30857  shaddcl  31204  shmulcl  31205  spansnss2  31562  cnopc  31900  cnfnc  31917  adj1  31920  pjorthcoi  32156  stj  32222  mdsl1i  32308  chirredlem1  32377  mdsymlem5  32394  cdj3lem2b  32424  slmdlema  33179  isprmidlc  33419  pconncn  35275  cvmlift2lem1  35353  fmla0xp  35434  ss2mcls  35619  antnestlaw2  35743  dfon2lem6  35837  waj-ax  36465  lukshef-ax2  36466  bj-alrim  36744  bj-nexdt  36748  sucneqond  37416  rdgssun  37429  ptrecube  37666  poimirlem26  37692  poimirlem29  37695  heiborlem1  37857  rngodm1dm2  37978  rngoueqz  37986  zerdivemp1x  37993  isdrngo3  38005  0rngo  38073  pridl  38083  ispridlc  38116  isdmn3  38120  dmnnzd  38121  elrelscnveq3  38645  lshpcmp  39093  omllaw  39348  dochexmidlem7  41571  lspindp5  41875  zdivgd  42436  fsuppind  42689  dfac21  43164  eexinst11  44625  ax6e2eq  44655  e222  44734  e111  44772  e333  44830  natlocalincr  46979  imarnf1pr  47387  2ffzoeq  47432  iccpartigtl  47528  iccpartgt  47532  lighneallem3  47712  lighneal  47716  requad1  47727  evenltle  47822  fppr2odd  47836  sgoldbeven3prm  47888  bgoldbtbndlem2  47911  isubgr3stgrlem4  48074  isubgr3stgrlem7  48077  gpgedg2iv  48172  lincdifsn  48530  lindslinindimp2lem4  48567  snlindsntor  48577  lincresunit3lem1  48585  lincresunit3lem2  48586  f002  48959  setrec1lem2  49794