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  2465  eupickbi  2661  ceqsalgALT  3486  cgsexg  3494  cgsex2g  3495  cgsex4g  3496  spcegv  3551  spc2egv  3553  disjne  4408  uneqdifeq  4448  preqsnd  4819  preq12nebg  4823  opthprneg  4825  dfiun2g  4988  axprlem4  5391  pocl  5571  relresfldOLD  6274  unixpid  6282  ordnbtwn  6453  sucssel  6455  ordelinel  6461  funmo  6549  fvimacnv  7045  ordsuc  7810  tfi  7849  focdmex  7953  f1ovv  7955  opreuopreu  8031  frrlem4  8288  tz7.49  8434  oeworde  8581  fsetprcnex  8863  dom2d  8999  findcard  9158  fisupg  9258  dffi3  9401  noinfep  9639  cantnflem2  9669  ttrcltr  9695  tcmin  9718  rankr1ag  9784  rankunb  9832  rankxpsuc  9864  alephordi  10077  alephsucdom  10082  alephinit  10098  dfac9  10139  ackbij2lem4  10243  cff1  10260  cfslbn  10269  cfcoflem  10274  cfcof  10276  infpssrlem5  10309  isfin7-2  10398  acncc  10442  domtriomlem  10444  axdc3lem2  10453  ttukeylem1  10511  iundom2g  10548  axpowndlem3  10608  wunex2  10747  grupr  10806  gruiun  10808  eltskm  10852  nqereu  10938  addcanpr  11055  axpre-sup  11178  relin01  11762  nneo  12705  zeo2  12708  xrub  13364  uznfz  13665  difelfzle  13696  ssfzo12  13815  facndiv  14352  hashgt12el2  14488  hash2prde  14535  hash2pwpr  14541  hashle2prv  14543  tpfo  14565  fi1uzind  14572  swrdswrd  14774  pfxccatin12lem2  14800  pfxccatin12  14802  pfxccat3  14803  cshwidxmod  14874  2cshwcshw  14896  fsumcom2  15860  fprodss  16035  fprodcom2  16071  ndvdssub  16499  eucalglt  16675  prmind2  16775  coprm  16802  prmdiveq  16877  prmdvdsprmop  17135  prmgaplem5  17147  cicsym  17893  drsdir  18390  lublecllem  18446  istos  18504  tsrlin  18673  dirge  18691  mhmlin  18901  issubg2  19265  nsgbi  19280  symgextf1lem  19547  sylow2a  19746  gsumpr  20082  0ringnnzr  20686  0ring01eq  20690  01eq0ringOLD  20692  nrhmzr  20699  issubrng2  20720  issubrg2  20754  isdrng5  20917  abvmul  20987  abvtri  20988  lmodlema  21049  rmodislmodlem  21113  rmodislmod  21114  ellspsn6  21178  lmhmlin  21219  lbsind  21264  isprmidlc  21535  nzerooringczr  21693  ipcj  21847  obsip  21934  lindsss  22037  mamufacex  22618  mavmulsolcl  22773  slesolvec  22904  inopn  23124  basis1  23175  tgss  23193  tgcl  23194  elcls3  23308  neindisj2  23348  cncls  23499  1stcelcls  23687  qtoptop2  23925  nrmr0reg  23975  fbasssin  24062  fbfinnfr  24067  fbunfip  24095  filufint  24146  uffix  24147  ufinffr  24155  ufilen  24156  fmfnfmlem1  24180  flftg  24222  alexsubALT  24277  xmeteq0  24564  blssexps  24652  blssex  24653  mopni3  24720  neibl  24727  metss  24734  metcnp3  24766  nmvs  24902  iccntr  25048  reconnlem2  25054  lebnumlem3  25191  caubl  25536  bcthlem5  25556  ovolunlem1  25725  voliunlem1  25778  volsuplem  25783  ellimc3  26106  logbgcd1irr  27031  lgsqrmodndvds  27589  gausslemma2dlem0i  27600  2lgsoddprmlem3  27650  dchrisumlema  27724  nofv  27893  nolesgn2o  27907  nogesgn1o  27909  nosupbnd1lem5  27948  addsprop  28241  negsprop  28300  mulsprop  28395  precsexlem6  28477  precsexlem7  28478  umgrnloopv  29563  usgrnloopvALT  29661  umgrres1lem  29770  upgrres1  29773  nbuhgr  29803  cplgrop  29897  fusgrregdegfi  30029  g0wlk0  30110  wlkdlem2  30141  upgrwlkdvdelem  30201  crctcshwlkn0lem3  30280  crctcshwlkn0lem5  30282  wspn0  30392  usgrwwlks2on  30426  umgrwwlks2on  30427  elwspths2spth  30438  clwlkclwwlklem2a  30468  clwlkclwwlklem3  30471  clwwlkn1loopb  30513  clwwlknonwwlknonb  30576  clwwlknonex2lem2  30578  3cyclfrgrrn2  30767  frgrncvvdeqlem8  30786  frgrwopregasn  30796  frgrwopregbsn  30797  frgrwopreg1  30798  frgrwopreg2  30799  frgrregord013  30875  frgrogt3nreg  30877  ablocom  31029  ubthlem1  31351  shaddcl  31698  shmulcl  31699  spansnss2  32056  cnopc  32394  cnfnc  32411  adj1  32414  pjorthcoi  32650  stj  32716  mdsl1i  32802  chirredlem1  32871  mdsymlem5  32888  cdj3lem2b  32918  slmdlema  33643  vonf1oonfo  35712  pconncn  35803  cvmlift2lem1  35881  fmla0xp  35962  ss2mcls  36147  antnestlaw2  36271  dfon2lem6  36365  waj-ax  37033  lukshef-ax2  37034  tr0elw  37103  bj-alrim  37426  bj-nexdt  37430  sucneqond  38119  rdgssun  38132  ptrecube  38369  poimirlem26  38395  poimirlem29  38398  heiborlem1  38561  rngodm1dm2  38682  rngoueqz  38690  zerdivemp1x  38697  isdrngo3  38709  0rngo  38777  pridl  38787  ispridlc  38820  isdmn3  38824  dmnnzd  38825  elrelscnveq3  39375  lshpcmp  39861  omllaw  40116  dochexmidlem7  42339  lspindp5  42643  zdivgd  43212  fsuppind  43436  dfac21  43907  eexinst11  45350  ax6e2eq  45380  e222  45459  e111  45497  e333  45555  imarnf1pr  48170  2ffzoeq  48216  iccpartigtl  48323  iccpartgt  48327  lighneallem3  48510  lighneal  48514  requad1  48538  evenltle  48633  fppr2odd  48647  sgoldbeven3prm  48699  bgoldbtbndlem2  48722  isubgr3stgrlem4  48885  isubgr3stgrlem7  48888  gpgedg2iv  48983  isidom3  49260  idomnzd  49261  lincdifsn  49354  lindslinindimp2lem4  49391  snlindsntor  49401  lincresunit3lem1  49409  lincresunit3lem2  49410  f002  49782  setrec1lem2  50614