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  2430  eupickbi  2625  ceqsalgALT  3499  cgsexg  3509  cgsex2g  3510  cgsex4g  3511  cgsex4gOLD  3512  cgsex4gOLDOLD  3513  spcegv  3583  spc2egv  3585  disjne  4459  uneqdifeq  4497  preqsnd  4865  preq12nebg  4869  opthprneg  4871  dfiun2g  5038  pocl  5601  relresfld  6287  unixpid  6295  ordnbtwn  6469  sucssel  6471  ordelinel  6477  funmo  6574  fvimacnv  7066  2f1fvneq  7275  ordsuc  7822  ordsucOLD  7823  tfi  7863  focdmex  7969  f1ovv  7971  opreuopreu  8048  frrlem4  8304  wfrlem4OLD  8342  wfrlem10OLD  8348  tz7.49  8475  oeworde  8623  fsetprcnex  8891  dom2d  9024  findcard  9201  fisupg  9325  dffi3  9474  noinfep  9703  cantnflem2  9733  ttrcltr  9759  tcmin  9784  rankr1ag  9845  rankunb  9893  rankxpsuc  9925  alephordi  10117  alephsucdom  10122  alephinit  10138  dfac9  10179  ackbij2lem4  10285  cff1  10301  cfslbn  10310  cfcoflem  10315  cfcof  10317  infpssrlem5  10350  isfin7-2  10439  acncc  10483  domtriomlem  10485  axdc3lem2  10494  ttukeylem1  10552  iundom2g  10583  axpowndlem3  10642  wunex2  10781  grupr  10840  gruiun  10842  eltskm  10886  nqereu  10972  addcanpr  11089  axpre-sup  11212  relin01  11788  nneo  12698  zeo2  12701  xrub  13345  uznfz  13638  difelfzle  13668  ssfzo12  13779  facndiv  14305  hashgt12el2  14440  hash2prde  14489  hash2pwpr  14495  hashle2prv  14497  fi1uzind  14516  swrdswrd  14713  pfxccatin12lem2  14739  pfxccatin12  14741  pfxccat3  14742  cshwidxmod  14811  2cshwcshw  14834  fsumcom2  15778  fprodss  15950  fprodcom2  15986  sumodd  16390  ndvdssub  16411  eucalglt  16586  prmind2  16686  coprm  16712  prmdiveq  16788  prmdvdsprmop  17045  prmgaplem5  17057  cicsym  17820  drsdir  18327  lublecllem  18385  istos  18443  tsrlin  18610  dirge  18628  mhmlin  18783  issubg2  19135  nsgbi  19151  symgextf1lem  19418  sylow2a  19617  gsumpr  19953  0ringnnzr  20507  0ring01eq  20511  01eq0ringOLD  20513  nrhmzr  20519  issubrng2  20540  issubrg2  20576  abvmul  20800  abvtri  20801  lmodlema  20841  rmodislmodlem  20905  rmodislmod  20906  rmodislmodOLD  20907  ellspsn6  20971  lmhmlin  21013  lbsind  21058  nzerooringczr  21470  ipcj  21630  obsip  21719  lindsss  21822  mamufacex  22387  mavmulsolcl  22544  slesolvec  22672  inopn  22892  basis1  22944  tgss  22962  tgcl  22963  elcls3  23078  neindisj2  23118  cncls  23269  1stcelcls  23456  qtoptop2  23694  nrmr0reg  23744  fbasssin  23831  fbfinnfr  23836  fbunfip  23864  filufint  23915  uffix  23916  ufinffr  23924  ufilen  23925  fmfnfmlem1  23949  flftg  23991  alexsubALT  24046  xmeteq0  24335  blssexps  24423  blssex  24424  mopni3  24494  neibl  24501  metss  24508  metcnp3  24540  nmvs  24684  iccntr  24828  reconnlem2  24834  lebnumlem3  24980  caubl  25327  bcthlem5  25347  ovolunlem1  25517  voliunlem1  25570  volsuplem  25575  ellimc3  25899  logbgcd1irr  26822  lgsqrmodndvds  27382  gausslemma2dlem0i  27393  2lgsoddprmlem3  27443  dchrisumlema  27517  nofv  27687  nolesgn2o  27701  nogesgn1o  27703  nosupbnd1lem5  27742  addsprop  27990  negsprop  28044  mulsprop  28131  precsexlem6  28211  precsexlem7  28212  umgrnloopv  29042  usgrnloopvALT  29137  umgrres1lem  29246  upgrres1  29249  nbuhgr  29279  cplgrop  29373  fusgrregdegfi  29506  g0wlk0  29589  wlkdlem2  29620  upgrwlkdvdelem  29673  crctcshwlkn0lem3  29746  crctcshwlkn0lem5  29748  wspn0  29858  umgrwwlks2on  29891  elwspths2spth  29901  clwlkclwwlklem2a  29931  clwlkclwwlklem3  29934  clwwlkn1loopb  29976  clwwlknonwwlknonb  30039  clwwlknonex2lem2  30041  3cyclfrgrrn2  30220  frgrncvvdeqlem8  30239  frgrwopregasn  30249  frgrwopregbsn  30250  frgrwopreg1  30251  frgrwopreg2  30252  frgrregord013  30328  frgrogt3nreg  30330  ablocom  30481  ubthlem1  30803  shaddcl  31150  shmulcl  31151  spansnss2  31508  cnopc  31846  cnfnc  31863  adj1  31866  pjorthcoi  32102  stj  32168  mdsl1i  32254  chirredlem1  32323  mdsymlem5  32340  cdj3lem2b  32370  slmdlema  33067  isprmidlc  33322  pconncn  35052  cvmlift2lem1  35130  fmla0xp  35211  ss2mcls  35396  dfon2lem6  35612  waj-ax  36126  lukshef-ax2  36127  bj-alrim  36398  bj-nexdt  36402  sucneqond  37072  rdgssun  37085  ptrecube  37321  poimirlem26  37347  poimirlem29  37350  heiborlem1  37512  rngodm1dm2  37633  rngoueqz  37641  zerdivemp1x  37648  isdrngo3  37660  0rngo  37728  pridl  37738  ispridlc  37771  isdmn3  37775  dmnnzd  37776  elrelscnveq3  38189  lshpcmp  38686  omllaw  38941  dochexmidlem7  41165  lspindp5  41469  fsuppind  42062  zdivgd  42132  dfac21  42727  eexinst11  44203  ax6e2eq  44233  e222  44312  e111  44350  e333  44409  natlocalincr  46495  tworepnotupword  46505  imarnf1pr  46895  2ffzoeq  46940  iccpartigtl  46995  iccpartgt  46999  lighneallem3  47179  lighneal  47183  requad1  47194  evenltle  47289  fppr2odd  47303  sgoldbeven3prm  47355  bgoldbtbndlem2  47378  lincdifsn  47807  lindslinindimp2lem4  47844  snlindsntor  47854  lincresunit3lem1  47862  lincresunit3lem2  47863  f002  48221  setrec1lem2  48434