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 ⊢ (𝜑 → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com12  33  syl5  35  speimfw  1996  axc16i  2466  eupickbi  2662  ceqsalgALT  3487  cgsexg  3495  cgsex2g  3496  cgsex4g  3497  spcegv  3552  spc2egv  3554  disjne  4408  uneqdifeq  4448  preqsnd  4819  preq12nebg  4823  opthprneg  4825  dfiun2g  4988  axprlem4  5388  pocl  5567  relresfldOLD  6278  unixpid  6286  ordnbtwn  6457  sucssel  6459  ordelinel  6465  funmo  6553  fvimacnv  7050  ordsuc  7823  tfi  7862  focdmex  7966  f1ovv  7968  opreuopreu  8044  frrlem4  8300  tz7.49  8448  oeworde  8595  fsetprcnex  8877  dom2d  9013  findcard  9172  fisupg  9272  dffi3  9416  noinfep  9654  cantnflem2  9684  ttrcltr  9710  tcmin  9733  rankr1ag  9803  rankunb  9857  rankxpsuc  9892  setrec1lem2  9960  alephordi  10146  alephsucdom  10151  alephinit  10167  dfac9  10208  ackbij2lem4  10312  cff1  10329  cfslbn  10338  cfcoflem  10343  cfcof  10345  infpssrlem5  10378  isfin7-2  10467  acncc  10511  domtriomlem  10513  axdc3lem2  10522  ttukeylem1  10580  iundom2g  10617  axpowndlem3  10677  wunex2  10816  grupr  10875  gruiun  10877  eltskm  10921  nqereu  11007  addcanpr  11124  axpre-sup  11247  relin01  11833  nneo  12776  zeo2  12779  xrub  13435  uznfz  13737  difelfzle  13768  ssfzo12  13887  facndiv  14425  hashgt12el2  14561  hash2prde  14608  hash2pwpr  14614  hashle2prv  14616  tpfo  14638  fi1uzind  14645  swrdswrd  14847  pfxccatin12lem2  14873  pfxccatin12  14875  pfxccat3  14876  cshwidxmod  14947  2cshwcshw  14969  fsumcom2  15933  fprodss  16108  fprodcom2  16144  ndvdssub  16572  eucalglt  16753  prmind2  16853  coprm  16880  prmdiveq  16956  prmdvdsprmop  17214  prmgaplem5  17226  cicsym  17972  drsdir  18469  lublecllem  18525  istos  18583  tsrlin  18752  dirge  18770  mhmlin  18981  issubg2  19345  nsgbi  19360  symgextf1lem  19627  sylow2a  19826  gsumpr  20162  0ringnnzr  20769  0ring01eq  20773  01eq0ringOLD  20775  nrhmzr  20782  issubrng2  20803  issubrg2  20837  isdrng5  21001  abvmul  21071  abvtri  21072  lmodlema  21133  rmodislmodlem  21197  rmodislmod  21198  ellspsn6  21262  lmhmlin  21303  lbsind  21348  isprmidlc  21621  nzerooringczr  21779  ipcj  21933  obsip  22020  lindsss  22123  mamufacex  22704  mavmulsolcl  22859  slesolvec  22990  inopn  23210  basis1  23261  tgss  23279  tgcl  23280  elcls3  23394  neindisj2  23434  cncls  23585  1stcelcls  23773  qtoptop2  24011  nrmr0reg  24061  fbasssin  24148  fbfinnfr  24153  fbunfip  24181  filufint  24232  uffix  24233  ufinffr  24241  ufilen  24242  fmfnfmlem1  24266  flftg  24308  alexsubALT  24363  xmeteq0  24650  blssexps  24738  blssex  24739  mopni3  24806  neibl  24813  metss  24820  metcnp3  24852  nmvs  24988  iccntr  25134  reconnlem2  25140  lebnumlem3  25277  caubl  25622  bcthlem5  25642  ovolunlem1  25811  voliunlem1  25864  volsuplem  25869  ellimc3  26192  logbgcd1irr  27115  lgsqrmodndvds  27673  gausslemma2dlem0i  27684  2lgsoddprmlem3  27734  dchrisumlema  27808  nofv  28007  nolesgn2o  28021  nogesgn1o  28023  nosupbnd1lem5  28062  addsprop  28355  negsprop  28414  mulsprop  28509  precsexlem6  28591  precsexlem7  28592  umgrnloopv  29677  usgrnloopvALT  29775  umgrres1lem  29884  upgrres1  29887  nbuhgr  29917  cplgrop  30011  fusgrregdegfi  30143  g0wlk0  30224  wlkdlem2  30255  upgrwlkdvdelem  30315  crctcshwlkn0lem3  30394  crctcshwlkn0lem5  30396  wspn0  30506  usgrwwlks2on  30540  umgrwwlks2on  30541  elwspths2spth  30552  clwlkclwwlklem2a  30582  clwlkclwwlklem3  30585  clwwlkn1loopb  30627  clwwlknonwwlknonb  30690  clwwlknonex2lem2  30692  3cyclfrgrrn2  30881  frgrncvvdeqlem8  30900  frgrwopregasn  30910  frgrwopregbsn  30911  frgrwopreg1  30912  frgrwopreg2  30913  frgrregord013  30989  frgrogt3nreg  30991  ablocom  31143  ubthlem1  31465  shaddcl  31812  shmulcl  31813  spansnss2  32170  cnopc  32508  cnfnc  32525  adj1  32528  pjorthcoi  32764  stj  32830  mdsl1i  32916  chirredlem1  32985  mdsymlem5  33002  cdj3lem2b  33032  slmdlema  33757  vonf1oonfo  35877  pconncn  35968  cvmlift2lem1  36046  fmla0xp  36127  ss2mcls  36312  antnestlaw2  36436  dfon2lem6  36530  waj-ax  37182  lukshef-ax2  37183  tr0elw  37252  bj-alrim  37575  bj-nexdt  37579  sucneqond  38268  rdgssun  38281  ptrecube  38518  poimirlem26  38544  poimirlem29  38547  heiborlem1  38725  rngodm1dm2  38846  rngoueqz  38854  zerdivemp1x  38861  isdrngo3  38873  0rngo  38941  pridl  38951  ispridlc  38984  isdmn3  38988  dmnnzd  38989  elrelscnveq3  39539  lshpcmp  40025  omllaw  40280  dochexmidlem7  42503  lspindp5  42807  zdivgd  43368  fsuppind  43598  dfac21  44052  eexinst11  45495  ax6e2eq  45525  e222  45604  e111  45642  e333  45700  imarnf1pr  48321  2ffzoeq  48367  iccpartigtl  48474  iccpartgt  48478  lighneallem3  48661  lighneal  48665  requad1  48689  evenltle  48784  fppr2odd  48798  sgoldbeven3prm  48850  bgoldbtbndlem2  48873  isubgr3stgrlem4  49036  isubgr3stgrlem7  49039  gpgedg2iv  49134  isidom3  49411  idomnzd  49412  lincdifsn  49505  lindslinindimp2lem4  49542  snlindsntor  49552  lincresunit3lem1  49560  lincresunit3lem2  49561  f002  49933