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  1972  sbequ2OLD  2249  axc16i  2435  eupickbi  2637  ceqsalgALT  3431  cgsexg  3440  cgsex2g  3441  cgsex4g  3442  cgsex4gOLD  3443  spcegv  3502  spc2egv  3504  disjne  4355  uneqdifeq  4390  preqsnd  4755  preq12nebg  4759  opthprneg  4761  pocl  5460  relresfld  6119  unixpid  6127  ordnbtwn  6281  sucssel  6283  ordelinel  6289  fvimacnv  6851  2f1fvneq  7050  ordsuc  7571  tfi  7610  fornex  7707  f1ovv  7709  opreuopreu  7784  frrlem4  8008  wfrlem4  8036  wfrlem10  8042  tz7.49  8159  oeworde  8299  fsetprcnex  8521  dom2d  8647  findcard  8819  fisupg  8897  dffi3  9025  noinfep  9253  cantnflem2  9283  tcmin  9335  rankr1ag  9383  rankunb  9431  rankxpsuc  9463  alephordi  9653  alephsucdom  9658  alephinit  9674  dfac9  9715  ackbij2lem4  9821  cff1  9837  cfslbn  9846  cfcoflem  9851  cfcof  9853  infpssrlem5  9886  isfin7-2  9975  acncc  10019  domtriomlem  10021  axdc3lem2  10030  ttukeylem1  10088  iundom2g  10119  axpowndlem3  10178  wunex2  10317  grupr  10376  gruiun  10378  eltskm  10422  nqereu  10508  addcanpr  10625  axpre-sup  10748  relin01  11321  nneo  12226  zeo2  12229  xrub  12867  uznfz  13160  difelfzle  13190  ssfzo12  13300  facndiv  13819  hashgt12el2  13955  hash2prde  14001  hash2pwpr  14007  hashle2prv  14009  fi1uzind  14028  swrdswrd  14235  pfxccatin12lem2  14261  pfxccatin12  14263  pfxccat3  14264  cshwidxmod  14333  2cshwcshw  14355  fsumcom2  15301  fprodss  15473  fprodcom2  15509  sumodd  15912  ndvdssub  15933  eucalglt  16105  prmind2  16205  coprm  16231  prmdiveq  16302  prmdvdsprmop  16559  prmgaplem5  16571  cicsym  17263  drsdir  17763  lublecllem  17820  istos  17878  tsrlin  18045  dirge  18063  mhmlin  18179  issubg2  18512  nsgbi  18527  symgextf1lem  18766  sylow2a  18962  gsumpr  19294  issubrg2  19774  abvmul  19819  abvtri  19820  lmodlema  19858  rmodislmodlem  19920  rmodislmod  19921  lspsnel6  19985  lmhmlin  20026  lbsind  20071  0ringnnzr  20261  0ring01eq  20263  01eq0ring  20264  ipcj  20550  obsip  20637  lindsss  20740  mamufacex  21242  mavmulsolcl  21402  slesolvec  21530  inopn  21750  basis1  21801  tgss  21819  tgcl  21820  elcls3  21934  neindisj2  21974  cncls  22125  1stcelcls  22312  qtoptop2  22550  nrmr0reg  22600  fbasssin  22687  fbfinnfr  22692  fbunfip  22720  filufint  22771  uffix  22772  ufinffr  22780  ufilen  22781  fmfnfmlem1  22805  flftg  22847  alexsubALT  22902  xmeteq0  23190  blssexps  23278  blssex  23279  mopni3  23346  neibl  23353  metss  23360  metcnp3  23392  nmvs  23528  iccntr  23672  reconnlem2  23678  lebnumlem3  23814  caubl  24159  bcthlem5  24179  ovolunlem1  24348  voliunlem1  24401  volsuplem  24406  ellimc3  24730  logbgcd1irr  25631  lgsqrmodndvds  26188  gausslemma2dlem0i  26199  2lgsoddprmlem3  26249  dchrisumlema  26323  umgrnloopv  27151  usgrnloopvALT  27243  umgrres1lem  27352  upgrres1  27355  nbuhgr  27385  cplgrop  27479  fusgrregdegfi  27611  g0wlk0  27693  wlkdlem2  27725  upgrwlkdvdelem  27777  crctcshwlkn0lem3  27850  crctcshwlkn0lem5  27852  wspn0  27962  umgrwwlks2on  27995  elwspths2spth  28005  clwlkclwwlklem2a  28035  clwlkclwwlklem3  28038  clwwlkn1loopb  28080  clwwlknonwwlknonb  28143  clwwlknonex2lem2  28145  3cyclfrgrrn2  28324  frgrncvvdeqlem8  28343  frgrwopregasn  28353  frgrwopregbsn  28354  frgrwopreg1  28355  frgrwopreg2  28356  frgrregord013  28432  frgrogt3nreg  28434  ablocom  28583  ubthlem1  28905  shaddcl  29252  shmulcl  29253  spansnss2  29610  cnopc  29948  cnfnc  29965  adj1  29968  pjorthcoi  30204  stj  30270  mdsl1i  30356  chirredlem1  30425  mdsymlem5  30442  cdj3lem2b  30472  slmdlema  31129  isprmidlc  31291  pconncn  32853  cvmlift2lem1  32931  fmla0xp  33012  ss2mcls  33197  dfon2lem6  33434  nofv  33546  nolesgn2o  33560  nogesgn1o  33562  nosupbnd1lem5  33601  waj-ax  34289  lukshef-ax2  34290  bj-alrim  34561  bj-nexdt  34565  sucneqond  35222  rdgssun  35235  ptrecube  35463  poimirlem26  35489  poimirlem29  35492  heiborlem1  35655  rngodm1dm2  35776  rngoueqz  35784  zerdivemp1x  35791  isdrngo3  35803  0rngo  35871  pridl  35881  ispridlc  35914  isdmn3  35918  dmnnzd  35919  elrelscnveq3  36295  lshpcmp  36688  omllaw  36943  dochexmidlem7  39166  lspindp5  39470  fsuppind  39930  dfac21  40535  eexinst11  41761  ax6e2eq  41791  e222  41870  e111  41908  e333  41967  imarnf1pr  44389  2ffzoeq  44436  iccpartigtl  44491  iccpartgt  44495  lighneallem3  44675  lighneal  44679  requad1  44690  evenltle  44785  fppr2odd  44799  sgoldbeven3prm  44851  bgoldbtbndlem2  44874  isomuspgrlem2b  44897  nrhmzr  45047  nzerooringczr  45246  lincdifsn  45381  lindslinindimp2lem4  45418  snlindsntor  45428  lincresunit3lem1  45436  lincresunit3lem2  45437  f002  45797  setrec1lem2  46008