Theorem syl5com 32

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 26	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
3		syl5com.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	sylcom 31	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  33  syl5  35  speimfw  1986  axc16i  2470  eupickbi  2666  ceqsalgALT  3493  cgsexg  3501  cgsex2g  3502  cgsex4g  3503  spcegv  3559  spc2egv  3561  disjne  4412  uneqdifeq  4449  preqsnd  4820  preq12nebg  4824  opthprneg  4826  dfiun2g  4990  axprlem4  5388  pocl  5568  relresfld  6267  unixpid  6275  ordnbtwn  6445  sucssel  6447  ordelinel  6453  funmo  6541  fvimacnv  7038  ordsuc  7798  tfi  7837  focdmex  7941  f1ovv  7943  opreuopreu  8019  frrlem4  8274  tz7.49  8420  oeworde  8567  fsetprcnex  8847  dom2d  8978  findcard  9136  fisupg  9236  dffi3  9379  noinfep  9617  cantnflem2  9647  ttrcltr  9673  tcmin  9696  rankr1ag  9762  rankunb  9810  rankxpsuc  9842  alephordi  10046  alephsucdom  10051  alephinit  10067  dfac9  10108  ackbij2lem4  10212  cff1  10230  cfslbn  10239  cfcoflem  10244  cfcof  10246  infpssrlem5  10279  isfin7-2  10368  acncc  10412  domtriomlem  10414  axdc3lem2  10423  ttukeylem1  10481  iundom2g  10512  axpowndlem3  10572  wunex2  10711  grupr  10770  gruiun  10772  eltskm  10816  nqereu  10902  addcanpr  11019  axpre-sup  11142  relin01  11726  nneo  12671  zeo2  12674  xrub  13329  uznfz  13629  difelfzle  13660  ssfzo12  13779  facndiv  14315  hashgt12el2  14450  hash2prde  14497  hash2pwpr  14503  hashle2prv  14505  tpfo  14527  fi1uzind  14534  swrdswrd  14732  pfxccatin12lem2  14758  pfxccatin12  14760  pfxccat3  14761  cshwidxmod  14830  2cshwcshw  14852  fsumcom2  15815  fprodss  15992  fprodcom2  16028  sumodd  16436  ndvdssub  16457  eucalglt  16633  prmind2  16733  coprm  16760  prmdiveq  16835  prmdvdsprmop  17093  prmgaplem5  17105  cicsym  17851  drsdir  18348  lublecllem  18404  istos  18462  tsrlin  18631  dirge  18649  mhmlin  18841  issubg2  19199  nsgbi  19214  symgextf1lem  19481  sylow2a  19680  gsumpr  20016  0ringnnzr  20600  0ring01eq  20604  01eq0ringOLD  20606  nrhmzr  20613  issubrng2  20634  issubrg2  20668  abvmul  20893  abvtri  20894  lmodlema  20955  rmodislmodlem  21019  rmodislmod  21020  ellspsn6  21084  lmhmlin  21125  lbsind  21170  isprmidlc  21434  nzerooringczr  21590  ipcj  21744  obsip  21831  lindsss  21934  mamufacex  22514  mavmulsolcl  22669  slesolvec  22797  inopn  23017  basis1  23068  tgss  23086  tgcl  23087  elcls3  23201  neindisj2  23241  cncls  23392  1stcelcls  23579  qtoptop2  23817  nrmr0reg  23867  fbasssin  23954  fbfinnfr  23959  fbunfip  23987  filufint  24038  uffix  24039  ufinffr  24047  ufilen  24048  fmfnfmlem1  24072  flftg  24114  alexsubALT  24169  xmeteq0  24456  blssexps  24544  blssex  24545  mopni3  24612  neibl  24619  metss  24626  metcnp3  24658  nmvs  24794  iccntr  24940  reconnlem2  24946  lebnumlem3  25083  caubl  25428  bcthlem5  25448  ovolunlem1  25617  voliunlem1  25670  volsuplem  25675  ellimc3  25999  logbgcd1irr  26917  lgsqrmodndvds  27475  gausslemma2dlem0i  27486  2lgsoddprmlem3  27536  dchrisumlema  27610  nofv  27779  nolesgn2o  27793  nogesgn1o  27795  nosupbnd1lem5  27834  addsprop  28127  negsprop  28186  mulsprop  28281  precsexlem6  28363  precsexlem7  28364  umgrnloopv  29365  usgrnloopvALT  29460  umgrres1lem  29569  upgrres1  29572  nbuhgr  29602  cplgrop  29696  fusgrregdegfi  29828  g0wlk0  29909  wlkdlem2  29940  upgrwlkdvdelem  29994  crctcshwlkn0lem3  30070  crctcshwlkn0lem5  30072  wspn0  30182  usgrwwlks2on  30216  umgrwwlks2on  30217  elwspths2spth  30228  clwlkclwwlklem2a  30258  clwlkclwwlklem3  30261  clwwlkn1loopb  30303  clwwlknonwwlknonb  30366  clwwlknonex2lem2  30368  3cyclfrgrrn2  30547  frgrncvvdeqlem8  30566  frgrwopregasn  30576  frgrwopregbsn  30577  frgrwopreg1  30578  frgrwopreg2  30579  frgrregord013  30655  frgrogt3nreg  30657  ablocom  30809  ubthlem1  31131  shaddcl  31478  shmulcl  31479  spansnss2  31836  cnopc  32174  cnfnc  32191  adj1  32194  pjorthcoi  32430  stj  32496  mdsl1i  32582  chirredlem1  32651  mdsymlem5  32668  cdj3lem2b  32698  slmdlema  33436  vonf1oonfo  35470  pconncn  35587  cvmlift2lem1  35665  fmla0xp  35746  ss2mcls  35931  antnestlaw2  36055  dfon2lem6  36149  waj-ax  36787  lukshef-ax2  36788  tr0elw  36857  bj-alrim  37180  bj-nexdt  37184  sucneqond  37871  rdgssun  37884  ptrecube  38131  poimirlem26  38157  poimirlem29  38160  heiborlem1  38322  rngodm1dm2  38443  rngoueqz  38451  zerdivemp1x  38458  isdrngo3  38470  0rngo  38538  pridl  38548  ispridlc  38581  isdmn3  38585  dmnnzd  38586  elrelscnveq3  39138  lshpcmp  39624  omllaw  39879  dochexmidlem7  42102  lspindp5  42406  zdivgd  42958  fsuppind  43184  dfac21  43655  eexinst11  45101  ax6e2eq  45131  e222  45210  e111  45248  e333  45306  natlocalincr  47450  imarnf1pr  47874  2ffzoeq  47920  iccpartigtl  48027  iccpartgt  48031  lighneallem3  48214  lighneal  48218  requad1  48242  evenltle  48337  fppr2odd  48351  sgoldbeven3prm  48403  bgoldbtbndlem2  48426  isubgr3stgrlem4  48589  isubgr3stgrlem7  48592  gpgedg2iv  48687  lincdifsn  49055  lindslinindimp2lem4  49092  snlindsntor  49102  lincresunit3lem1  49110  lincresunit3lem2  49111  f002  49483  setrec1lem2  50317