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  1965  axc16i  2433  eupickbi  2630  ceqsalgALT  3507  cgsexg  3517  cgsex2g  3518  cgsex4g  3519  cgsex4gOLD  3520  cgsex4gOLDOLD  3521  spcegv  3586  spc2egv  3588  disjne  4453  uneqdifeq  4491  preqsnd  4858  preq12nebg  4862  opthprneg  4864  dfiun2g  5032  pocl  5594  relresfld  6274  unixpid  6282  ordnbtwn  6456  sucssel  6458  ordelinel  6464  funmo  6562  fvimacnv  7053  2f1fvneq  7261  ordsuc  7803  ordsucOLD  7804  tfi  7844  focdmex  7944  f1ovv  7946  opreuopreu  8022  frrlem4  8276  wfrlem4OLD  8314  wfrlem10OLD  8320  tz7.49  8447  oeworde  8595  fsetprcnex  8858  dom2d  8991  findcard  9165  fisupg  9293  dffi3  9428  noinfep  9657  cantnflem2  9687  ttrcltr  9713  tcmin  9738  rankr1ag  9799  rankunb  9847  rankxpsuc  9879  alephordi  10071  alephsucdom  10076  alephinit  10092  dfac9  10133  ackbij2lem4  10239  cff1  10255  cfslbn  10264  cfcoflem  10269  cfcof  10271  infpssrlem5  10304  isfin7-2  10393  acncc  10437  domtriomlem  10439  axdc3lem2  10448  ttukeylem1  10506  iundom2g  10537  axpowndlem3  10596  wunex2  10735  grupr  10794  gruiun  10796  eltskm  10840  nqereu  10926  addcanpr  11043  axpre-sup  11166  relin01  11742  nneo  12650  zeo2  12653  xrub  13295  uznfz  13588  difelfzle  13618  ssfzo12  13729  facndiv  14252  hashgt12el2  14387  hash2prde  14435  hash2pwpr  14441  hashle2prv  14443  fi1uzind  14462  swrdswrd  14659  pfxccatin12lem2  14685  pfxccatin12  14687  pfxccat3  14688  cshwidxmod  14757  2cshwcshw  14780  fsumcom2  15724  fprodss  15896  fprodcom2  15932  sumodd  16335  ndvdssub  16356  eucalglt  16526  prmind2  16626  coprm  16652  prmdiveq  16723  prmdvdsprmop  16980  prmgaplem5  16992  cicsym  17755  drsdir  18259  lublecllem  18317  istos  18375  tsrlin  18542  dirge  18560  mhmlin  18715  issubg2  19057  nsgbi  19073  symgextf1lem  19329  sylow2a  19528  gsumpr  19864  0ringnnzr  20414  0ring01eq  20418  01eq0ringOLD  20420  issubrng2  20446  issubrg2  20482  abvmul  20580  abvtri  20581  lmodlema  20619  rmodislmodlem  20683  rmodislmod  20684  rmodislmodOLD  20685  lspsnel6  20749  lmhmlin  20790  lbsind  20835  ipcj  21406  obsip  21495  lindsss  21598  mamufacex  22111  mavmulsolcl  22273  slesolvec  22401  inopn  22621  basis1  22673  tgss  22691  tgcl  22692  elcls3  22807  neindisj2  22847  cncls  22998  1stcelcls  23185  qtoptop2  23423  nrmr0reg  23473  fbasssin  23560  fbfinnfr  23565  fbunfip  23593  filufint  23644  uffix  23645  ufinffr  23653  ufilen  23654  fmfnfmlem1  23678  flftg  23720  alexsubALT  23775  xmeteq0  24064  blssexps  24152  blssex  24153  mopni3  24223  neibl  24230  metss  24237  metcnp3  24269  nmvs  24413  iccntr  24557  reconnlem2  24563  lebnumlem3  24709  caubl  25056  bcthlem5  25076  ovolunlem1  25246  voliunlem1  25299  volsuplem  25304  ellimc3  25628  logbgcd1irr  26535  lgsqrmodndvds  27092  gausslemma2dlem0i  27103  2lgsoddprmlem3  27153  dchrisumlema  27227  nofv  27396  nolesgn2o  27410  nogesgn1o  27412  nosupbnd1lem5  27451  addsprop  27698  negsprop  27748  mulsprop  27825  precsexlem6  27897  precsexlem7  27898  umgrnloopv  28633  usgrnloopvALT  28725  umgrres1lem  28834  upgrres1  28837  nbuhgr  28867  cplgrop  28961  fusgrregdegfi  29093  g0wlk0  29176  wlkdlem2  29207  upgrwlkdvdelem  29260  crctcshwlkn0lem3  29333  crctcshwlkn0lem5  29335  wspn0  29445  umgrwwlks2on  29478  elwspths2spth  29488  clwlkclwwlklem2a  29518  clwlkclwwlklem3  29521  clwwlkn1loopb  29563  clwwlknonwwlknonb  29626  clwwlknonex2lem2  29628  3cyclfrgrrn2  29807  frgrncvvdeqlem8  29826  frgrwopregasn  29836  frgrwopregbsn  29837  frgrwopreg1  29838  frgrwopreg2  29839  frgrregord013  29915  frgrogt3nreg  29917  ablocom  30068  ubthlem1  30390  shaddcl  30737  shmulcl  30738  spansnss2  31095  cnopc  31433  cnfnc  31450  adj1  31453  pjorthcoi  31689  stj  31755  mdsl1i  31841  chirredlem1  31910  mdsymlem5  31927  cdj3lem2b  31957  slmdlema  32618  isprmidlc  32840  pconncn  34513  cvmlift2lem1  34591  fmla0xp  34672  ss2mcls  34857  dfon2lem6  35064  waj-ax  35602  lukshef-ax2  35603  bj-alrim  35874  bj-nexdt  35878  sucneqond  36549  rdgssun  36562  ptrecube  36791  poimirlem26  36817  poimirlem29  36820  heiborlem1  36982  rngodm1dm2  37103  rngoueqz  37111  zerdivemp1x  37118  isdrngo3  37130  0rngo  37198  pridl  37208  ispridlc  37241  isdmn3  37245  dmnnzd  37246  elrelscnveq3  37664  lshpcmp  38161  omllaw  38416  dochexmidlem7  40640  lspindp5  40944  fsuppind  41464  dfac21  42110  eexinst11  43590  ax6e2eq  43620  e222  43699  e111  43737  e333  43796  natlocalincr  45888  tworepnotupword  45898  imarnf1pr  46288  2ffzoeq  46334  iccpartigtl  46389  iccpartgt  46393  lighneallem3  46573  lighneal  46577  requad1  46588  evenltle  46683  fppr2odd  46697  sgoldbeven3prm  46749  bgoldbtbndlem2  46772  isomuspgrlem2b  46795  nrhmzr  46910  nzerooringczr  47058  lincdifsn  47192  lindslinindimp2lem4  47229  snlindsntor  47239  lincresunit3lem1  47247  lincresunit3lem2  47248  f002  47607  setrec1lem2  47820