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  1876  axc11nlemOLD2  1988  axc11nlemOLD  2160  axc11nlemALT  2306  axc11nOLD  2308  axc11nOLDOLD  2309  axc11nALT  2310  axc16i  2322  eupickbi  2539  ceqsalgALT  3231  cgsexg  3238  cgsex2g  3239  cgsex4g  3240  spc2egv  3295  spc3egv  3297  disjne  4022  uneqdifeq  4057  uneqdifeqOLD  4058  relresfld  5662  unixpid  5670  ordnbtwn  5816  sucssel  5819  ordelinel  5825  fvimacnv  6332  2f1fvneq  6517  ordsuc  7014  tfi  7053  fornex  7135  f1ovv  7137  wfrlem4  7418  wfrlem10  7424  tz7.49  7540  oeworde  7673  dom2d  7996  findcard  8199  fisupg  8208  dffi3  8337  fiinfg  8405  noinfep  8557  cantnflem2  8587  tcmin  8617  rankr1ag  8665  rankelb  8687  rankunb  8713  rankxpsuc  8745  alephordi  8897  alephsucdom  8902  alephinit  8918  dfac9  8958  ackbij2lem4  9064  cff1  9080  cfslbn  9089  cfcoflem  9094  cfcof  9096  infpssrlem5  9129  isfin7-2  9218  acncc  9262  domtriomlem  9264  axdc3lem2  9273  ttukeylem1  9331  iundom2g  9362  axpowndlem3  9421  wunex2  9560  grupr  9619  gruiun  9621  eltskm  9665  nqereu  9751  addcanpr  9868  axpre-sup  9990  relin01  10552  nneo  11461  zeo2  11464  xrub  12142  uznfz  12423  difelfzle  12452  ssfzo12  12561  facndiv  13075  hashf1rnOLD  13143  hashgt12el2  13211  hash2prde  13252  hash2pwpr  13258  hashle2prv  13260  fi1uzind  13279  fi1uzindOLD  13285  swrdswrd  13460  swrdccatin2  13487  swrdccatin12lem2  13489  swrdccatin12  13491  swrdccat3  13492  swrdccatid  13497  repswswrd  13531  2cshwcshw  13571  relexpcnvd  13776  relexpdmd  13784  relexprnd  13788  relexpfldd  13790  relexpaddd  13794  fsumcom2  14505  fsumcom2OLD  14506  fprodss  14678  fprodcom2  14714  fprodcom2OLD  14715  sumodd  15111  ndvdssub  15133  eucalglt  15298  prmind2  15398  coprm  15423  prmdiveq  15491  prmdvdsprmop  15747  prmgaplem5  15759  drsdir  16935  lublecllem  16988  istos  17035  tsrlin  17219  dirge  17237  mhmlin  17342  issubg2  17609  nsgbi  17625  symgextf1lem  17840  sylow2a  18034  issubrg2  18800  abvmul  18829  abvtri  18830  lmodlema  18868  rmodislmodlem  18930  rmodislmod  18931  lspsnel6  18994  lmhmlin  19035  lbsind  19080  0ring01eq  19271  01eq0ring  19272  gsummoncoe1  19674  ipcj  19979  obsip  20065  lindsss  20163  mamufacex  20195  mavmulsolcl  20357  slesolvec  20485  inopn  20704  basis1  20754  tgss  20772  tgcl  20773  elcls3  20887  neindisj2  20927  cncls  21078  1stcelcls  21264  qtoptop2  21502  nrmr0reg  21552  fbasssin  21640  fbfinnfr  21645  fbunfip  21673  filufint  21724  uffix  21725  ufinffr  21733  ufilen  21734  fmfnfmlem1  21758  flftg  21800  alexsubALT  21855  xmeteq0  22143  blssexps  22231  blssex  22232  mopni3  22299  neibl  22306  metss  22313  metcnp3  22345  nmvs  22480  reperflem  22621  iccntr  22624  reconnlem2  22630  lebnumlem3  22762  caubl  23106  bcthlem5  23125  ovolunlem1  23265  voliunlem1  23318  volsuplem  23323  ellimc3  23643  lhop1lem  23776  ulmss  24151  2lgsoddprmlem3  25139  dchrisumlema  25177  umgrnloopv  26001  usgrnloopvALT  26093  umgrres1lem  26202  upgrres1  26205  nbuhgr  26239  cplgrop  26333  fusgrregdegfi  26465  g0wlk0  26548  wlkdlem2  26580  upgrwlkdvdelem  26632  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  umgrwwlks2on  26850  elwspths2spth  26862  clwlkclwwlklem2a  26899  clwlkclwwlklem3  26902  clwlksfclwwlk  26962  3cyclfrgrrn2  27151  frgrncvvdeqlem8  27170  frgrwopregasn  27180  frgrwopregbsn  27181  frgrwopreg1  27182  frgrwopreg2  27183  numclwwlkovf2exlem2  27212  frgrregord013  27253  frgrogt3nreg  27255  ablocom  27402  ubthlem1  27726  shaddcl  28074  shmulcl  28075  spansnss2  28434  cnopc  28772  cnfnc  28789  adj1  28792  pjorthcoi  29028  stj  29094  mdsl1i  29180  chirredlem1  29249  mdsymlem5  29266  cdj3lem2b  29296  slmdlema  29756  pconncn  31206  cvmlift2lem1  31284  ss2mcls  31465  dfon2lem6  31693  frrlem4  31783  nofv  31810  nolesgn2o  31824  nosupbnd1lem5  31858  nn0prpw  32318  waj-ax  32413  lukshef-ax2  32414  bj-alrim  32683  bj-nexdt  32687  sucneqond  33213  ptrecube  33409  poimirlem26  33435  poimirlem29  33438  heiborlem1  33610  rngodm1dm2  33731  rngoueqz  33739  zerdivemp1x  33746  isdrngo3  33758  0rngo  33826  pridl  33836  ispridlc  33869  isdmn3  33873  dmnnzd  33874  lshpcmp  34275  omllaw  34530  dochexmidlem7  36755  lspindp5  37059  dfac21  37636  eexinst11  38733  ax6e2eq  38773  e222  38861  e111  38899  e333  38960  imarnf1pr  41301  2ffzoeq  41338  iccpartigtl  41359  iccpartgt  41363  pfxccatin12lem2  41424  pfxccatin12  41425  pfxccat3  41426  lighneallem3  41524  lighneal  41528  evenltle  41626  sgoldbeven3prm  41671  bgoldbtbndlem2  41694  nrhmzr  41873  nzerooringczr  42072  gsumpr  42139  lincdifsn  42213  snlindsntor  42260  lincresunit3lem1  42268  lincresunit3lem2  42269  lincresunit3  42270  setrec1lem2  42435