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  1925  sbequ2  2178  axc16i  2373  eupickbi  2667  ceqsalgALT  3444  cgsexg  3451  cgsex2g  3452  cgsex4g  3453  spcegv  3509  spc2egv  3511  disjne  4281  uneqdifeq  4315  preqsnd  4659  preq12nebg  4663  opthprneg  4665  relresfld  5962  unixpid  5970  ordnbtwn  6116  sucssel  6118  ordelinel  6124  fvimacnv  6646  2f1fvneq  6841  ordsuc  7343  tfi  7382  fornex  7467  f1ovv  7469  opreuopreu  7544  wfrlem4  7759  wfrlem4OLD  7760  wfrlem10  7766  tz7.49  7882  oeworde  8018  dom2d  8345  findcard  8550  fisupg  8559  dffi3  8688  noinfep  8915  cantnflem2  8945  tcmin  8975  rankr1ag  9023  rankunb  9071  rankxpsuc  9103  alephordi  9292  alephsucdom  9297  alephinit  9313  dfac9  9354  ackbij2lem4  9460  cff1  9476  cfslbn  9485  cfcoflem  9490  cfcof  9492  infpssrlem5  9525  isfin7-2  9614  acncc  9658  domtriomlem  9660  axdc3lem2  9669  ttukeylem1  9727  iundom2g  9758  axpowndlem3  9817  wunex2  9956  grupr  10015  gruiun  10017  eltskm  10061  nqereu  10147  addcanpr  10264  axpre-sup  10387  relin01  10963  nneo  11877  zeo2  11880  xrub  12519  uznfz  12804  difelfzle  12834  ssfzo12  12943  facndiv  13461  hashgt12el2  13595  hash2prde  13637  hash2pwpr  13643  hashle2prv  13645  fi1uzind  13664  swrdswrd  13885  pfxccatin12lem2  13929  swrdccatin12lem2OLD  13930  pfxccatin12  13932  swrdccatin12OLD  13933  pfxccat3  13934  swrdccat3OLD  13935  swrdccatidOLD  13946  2cshwcshw  14047  relexpcnvd  14254  relexpdmd  14262  relexprnd  14266  relexpfldd  14268  relexpaddd  14272  fsumcom2  14987  fprodss  15160  fprodcom2  15196  sumodd  15597  ndvdssub  15618  eucalglt  15783  prmind2  15883  coprm  15909  prmdiveq  15977  prmdvdsprmop  16233  prmgaplem5  16245  cicsym  16944  drsdir  17415  lublecllem  17468  istos  17515  tsrlin  17699  dirge  17717  mhmlin  17822  issubg2  18090  nsgbi  18106  symgextf1lem  18321  sylow2a  18517  gsumpr  18840  issubrg2  19290  abvmul  19334  abvtri  19335  lmodlema  19373  rmodislmodlem  19435  rmodislmod  19436  lspsnel6  19500  lmhmlin  19541  lbsind  19586  0ringnnzr  19775  0ring01eq  19777  01eq0ring  19778  ipcj  20495  obsip  20582  lindsss  20685  mamufacex  20717  mavmulsolcl  20879  slesolvec  21007  inopn  21226  basis1  21277  tgss  21295  tgcl  21296  elcls3  21410  neindisj2  21450  cncls  21601  1stcelcls  21788  qtoptop2  22026  nrmr0reg  22076  fbasssin  22163  fbfinnfr  22168  fbunfip  22196  filufint  22247  uffix  22248  ufinffr  22256  ufilen  22257  fmfnfmlem1  22281  flftg  22323  alexsubALT  22378  xmeteq0  22666  blssexps  22754  blssex  22755  mopni3  22822  neibl  22829  metss  22836  metcnp3  22868  nmvs  23003  iccntr  23147  reconnlem2  23153  lebnumlem3  23285  caubl  23629  bcthlem5  23649  ovolunlem1  23816  voliunlem1  23869  volsuplem  23874  ellimc3  24195  logbgcd1irr  25088  lgsqrmodndvds  25646  gausslemma2dlem0i  25657  2lgsoddprmlem3  25707  dchrisumlema  25781  umgrnloopv  26609  usgrnloopvALT  26701  umgrres1lem  26810  upgrres1  26813  nbuhgr  26843  cplgrop  26937  fusgrregdegfi  27069  g0wlk0  27151  wlkdlem2  27186  upgrwlkdvdelem  27240  crctcshwlkn0lem3  27313  crctcshwlkn0lem5  27315  wspn0  27445  umgrwwlks2on  27478  elwspths2spth  27488  clwlkclwwlklem2a  27519  clwlkclwwlklem3  27522  clwwlkn1loopb  27574  clwwlknonex2lem2  27651  3cyclfrgrrn2  27836  frgrncvvdeqlem8  27855  frgrwopregasn  27865  frgrwopregbsn  27866  frgrwopreg1  27867  frgrwopreg2  27868  frgrregord013  27967  frgrogt3nreg  27969  ablocom  28117  ubthlem1  28440  shaddcl  28788  shmulcl  28789  spansnss2  29148  cnopc  29486  cnfnc  29503  adj1  29506  pjorthcoi  29742  stj  29808  mdsl1i  29894  chirredlem1  29963  mdsymlem5  29980  cdj3lem2b  30010  slmdlema  30529  pconncn  32093  cvmlift2lem1  32171  fmla0xp  32230  ss2mcls  32372  dfon2lem6  32590  frrlem4  32684  nofv  32722  nolesgn2o  32736  nosupbnd1lem5  32770  waj-ax  33319  lukshef-ax2  33320  bj-alrim  33574  bj-nexdt  33578  bj-epelg  33907  sucneqond  34125  rdgssun  34138  ptrecube  34370  poimirlem26  34396  poimirlem29  34399  heiborlem1  34568  rngodm1dm2  34689  rngoueqz  34697  zerdivemp1x  34704  isdrngo3  34716  0rngo  34784  pridl  34794  ispridlc  34827  isdmn3  34831  dmnnzd  34832  elrelscnveq3  35213  lshpcmp  35606  omllaw  35861  dochexmidlem7  38084  lspindp5  38388  dfac21  39100  eexinst11  40318  ax6e2eq  40348  e222  40427  e111  40465  e333  40524  imarnf1pr  42921  2ffzoeq  42968  iccpartigtl  42989  iccpartgt  42993  lighneallem3  43174  lighneal  43178  requad1  43189  evenltle  43284  fppr2odd  43298  sgoldbeven3prm  43350  bgoldbtbndlem2  43373  isomuspgrlem2b  43396  nrhmzr  43542  nzerooringczr  43741  lincdifsn  43880  lindslinindimp2lem4  43917  snlindsntor  43927  lincresunit3lem1  43935  lincresunit3lem2  43936  setrec1lem2  44192