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  1960  axc16i  2438  eupickbi  2633  ceqsalgALT  3515  cgsexg  3523  cgsex2g  3524  cgsex4g  3525  cgsex4gOLD  3526  spcegv  3596  spc2egv  3598  disjne  4460  uneqdifeq  4498  preqsnd  4863  preq12nebg  4867  opthprneg  4869  dfiun2g  5034  axprlem4  5431  pocl  5604  relresfld  6297  unixpid  6305  ordnbtwn  6478  sucssel  6480  ordelinel  6486  funmo  6582  fvimacnv  7072  2f1fvneq  7279  ordsuc  7832  ordsucOLD  7833  tfi  7873  focdmex  7978  f1ovv  7980  opreuopreu  8057  frrlem4  8312  wfrlem4OLD  8350  wfrlem10OLD  8356  tz7.49  8483  oeworde  8629  fsetprcnex  8900  dom2d  9031  findcard  9201  fisupg  9321  dffi3  9468  noinfep  9697  cantnflem2  9727  ttrcltr  9753  tcmin  9778  rankr1ag  9839  rankunb  9887  rankxpsuc  9919  alephordi  10111  alephsucdom  10116  alephinit  10132  dfac9  10174  ackbij2lem4  10278  cff1  10295  cfslbn  10304  cfcoflem  10309  cfcof  10311  infpssrlem5  10344  isfin7-2  10433  acncc  10477  domtriomlem  10479  axdc3lem2  10488  ttukeylem1  10546  iundom2g  10577  axpowndlem3  10636  wunex2  10775  grupr  10834  gruiun  10836  eltskm  10880  nqereu  10966  addcanpr  11083  axpre-sup  11206  relin01  11784  nneo  12699  zeo2  12702  xrub  13350  uznfz  13646  difelfzle  13677  ssfzo12  13794  facndiv  14323  hashgt12el2  14458  hash2prde  14505  hash2pwpr  14511  hashle2prv  14513  tpfo  14535  fi1uzind  14542  swrdswrd  14739  pfxccatin12lem2  14765  pfxccatin12  14767  pfxccat3  14768  cshwidxmod  14837  2cshwcshw  14860  fsumcom2  15806  fprodss  15980  fprodcom2  16016  sumodd  16421  ndvdssub  16442  eucalglt  16618  prmind2  16718  coprm  16744  prmdiveq  16819  prmdvdsprmop  17076  prmgaplem5  17088  cicsym  17851  drsdir  18359  lublecllem  18417  istos  18475  tsrlin  18642  dirge  18660  mhmlin  18818  issubg2  19171  nsgbi  19187  symgextf1lem  19452  sylow2a  19651  gsumpr  19987  0ringnnzr  20541  0ring01eq  20545  01eq0ringOLD  20547  nrhmzr  20553  issubrng2  20574  issubrg2  20608  abvmul  20838  abvtri  20839  lmodlema  20879  rmodislmodlem  20943  rmodislmod  20944  rmodislmodOLD  20945  ellspsn6  21009  lmhmlin  21051  lbsind  21096  nzerooringczr  21508  ipcj  21669  obsip  21758  lindsss  21861  mamufacex  22415  mavmulsolcl  22572  slesolvec  22700  inopn  22920  basis1  22972  tgss  22990  tgcl  22991  elcls3  23106  neindisj2  23146  cncls  23297  1stcelcls  23484  qtoptop2  23722  nrmr0reg  23772  fbasssin  23859  fbfinnfr  23864  fbunfip  23892  filufint  23943  uffix  23944  ufinffr  23952  ufilen  23953  fmfnfmlem1  23977  flftg  24019  alexsubALT  24074  xmeteq0  24363  blssexps  24451  blssex  24452  mopni3  24522  neibl  24529  metss  24536  metcnp3  24568  nmvs  24712  iccntr  24856  reconnlem2  24862  lebnumlem3  25008  caubl  25355  bcthlem5  25375  ovolunlem1  25545  voliunlem1  25598  volsuplem  25603  ellimc3  25928  logbgcd1irr  26851  lgsqrmodndvds  27411  gausslemma2dlem0i  27422  2lgsoddprmlem3  27472  dchrisumlema  27546  nofv  27716  nolesgn2o  27730  nogesgn1o  27732  nosupbnd1lem5  27771  addsprop  28023  negsprop  28081  mulsprop  28170  precsexlem6  28250  precsexlem7  28251  umgrnloopv  29137  usgrnloopvALT  29232  umgrres1lem  29341  upgrres1  29344  nbuhgr  29374  cplgrop  29468  fusgrregdegfi  29601  g0wlk0  29684  wlkdlem2  29715  upgrwlkdvdelem  29768  crctcshwlkn0lem3  29841  crctcshwlkn0lem5  29843  wspn0  29953  umgrwwlks2on  29986  elwspths2spth  29996  clwlkclwwlklem2a  30026  clwlkclwwlklem3  30029  clwwlkn1loopb  30071  clwwlknonwwlknonb  30134  clwwlknonex2lem2  30136  3cyclfrgrrn2  30315  frgrncvvdeqlem8  30334  frgrwopregasn  30344  frgrwopregbsn  30345  frgrwopreg1  30346  frgrwopreg2  30347  frgrregord013  30423  frgrogt3nreg  30425  ablocom  30576  ubthlem1  30898  shaddcl  31245  shmulcl  31246  spansnss2  31603  cnopc  31941  cnfnc  31958  adj1  31961  pjorthcoi  32197  stj  32263  mdsl1i  32349  chirredlem1  32418  mdsymlem5  32435  cdj3lem2b  32465  slmdlema  33191  isprmidlc  33454  pconncn  35208  cvmlift2lem1  35286  fmla0xp  35367  ss2mcls  35552  dfon2lem6  35769  waj-ax  36396  lukshef-ax2  36397  bj-alrim  36675  bj-nexdt  36679  sucneqond  37347  rdgssun  37360  ptrecube  37606  poimirlem26  37632  poimirlem29  37635  heiborlem1  37797  rngodm1dm2  37918  rngoueqz  37926  zerdivemp1x  37933  isdrngo3  37945  0rngo  38013  pridl  38023  ispridlc  38056  isdmn3  38060  dmnnzd  38061  elrelscnveq3  38472  lshpcmp  38969  omllaw  39224  dochexmidlem7  41448  lspindp5  41752  zdivgd  42350  fsuppind  42576  dfac21  43054  eexinst11  44524  ax6e2eq  44554  e222  44633  e111  44671  e333  44730  natlocalincr  46829  tworepnotupword  46839  imarnf1pr  47231  2ffzoeq  47276  iccpartigtl  47347  iccpartgt  47351  lighneallem3  47531  lighneal  47535  requad1  47546  evenltle  47641  fppr2odd  47655  sgoldbeven3prm  47707  bgoldbtbndlem2  47730  isubgr3stgrlem4  47871  isubgr3stgrlem7  47874  lincdifsn  48269  lindslinindimp2lem4  48306  snlindsntor  48316  lincresunit3lem1  48324  lincresunit3lem2  48325  f002  48683  setrec1lem2  48918