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  7046  ordsuc  7811  tfi  7850  focdmex  7954  f1ovv  7956  opreuopreu  8032  frrlem4  8289  tz7.49  8437  oeworde  8584  fsetprcnex  8866  dom2d  9002  findcard  9161  fisupg  9261  dffi3  9404  noinfep  9642  cantnflem2  9672  ttrcltr  9698  tcmin  9721  rankr1ag  9787  rankunb  9835  rankxpsuc  9867  alephordi  10080  alephsucdom  10085  alephinit  10101  dfac9  10142  ackbij2lem4  10246  cff1  10263  cfslbn  10272  cfcoflem  10277  cfcof  10279  infpssrlem5  10312  isfin7-2  10401  acncc  10445  domtriomlem  10447  axdc3lem2  10456  ttukeylem1  10514  iundom2g  10551  axpowndlem3  10611  wunex2  10750  grupr  10809  gruiun  10811  eltskm  10855  nqereu  10941  addcanpr  11058  axpre-sup  11181  relin01  11765  nneo  12708  zeo2  12711  xrub  13367  uznfz  13668  difelfzle  13699  ssfzo12  13818  facndiv  14355  hashgt12el2  14491  hash2prde  14538  hash2pwpr  14544  hashle2prv  14546  tpfo  14568  fi1uzind  14575  swrdswrd  14777  pfxccatin12lem2  14803  pfxccatin12  14805  pfxccat3  14806  cshwidxmod  14877  2cshwcshw  14899  fsumcom2  15863  fprodss  16038  fprodcom2  16074  ndvdssub  16502  eucalglt  16678  prmind2  16778  coprm  16805  prmdiveq  16880  prmdvdsprmop  17138  prmgaplem5  17150  cicsym  17896  drsdir  18393  lublecllem  18449  istos  18507  tsrlin  18676  dirge  18694  mhmlin  18904  issubg2  19268  nsgbi  19283  symgextf1lem  19550  sylow2a  19749  gsumpr  20085  0ringnnzr  20689  0ring01eq  20693  01eq0ringOLD  20695  nrhmzr  20702  issubrng2  20723  issubrg2  20757  isdrng5  20920  abvmul  20990  abvtri  20991  lmodlema  21052  rmodislmodlem  21116  rmodislmod  21117  ellspsn6  21181  lmhmlin  21222  lbsind  21267  isprmidlc  21538  nzerooringczr  21696  ipcj  21850  obsip  21937  lindsss  22040  mamufacex  22621  mavmulsolcl  22776  slesolvec  22907  inopn  23127  basis1  23178  tgss  23196  tgcl  23197  elcls3  23311  neindisj2  23351  cncls  23502  1stcelcls  23690  qtoptop2  23928  nrmr0reg  23978  fbasssin  24065  fbfinnfr  24070  fbunfip  24098  filufint  24149  uffix  24150  ufinffr  24158  ufilen  24159  fmfnfmlem1  24183  flftg  24225  alexsubALT  24280  xmeteq0  24567  blssexps  24655  blssex  24656  mopni3  24723  neibl  24730  metss  24737  metcnp3  24769  nmvs  24905  iccntr  25051  reconnlem2  25057  lebnumlem3  25194  caubl  25539  bcthlem5  25559  ovolunlem1  25728  voliunlem1  25781  volsuplem  25786  ellimc3  26109  logbgcd1irr  27034  lgsqrmodndvds  27592  gausslemma2dlem0i  27603  2lgsoddprmlem3  27653  dchrisumlema  27727  nofv  27896  nolesgn2o  27910  nogesgn1o  27912  nosupbnd1lem5  27951  addsprop  28244  negsprop  28303  mulsprop  28398  precsexlem6  28480  precsexlem7  28481  umgrnloopv  29566  usgrnloopvALT  29664  umgrres1lem  29773  upgrres1  29776  nbuhgr  29806  cplgrop  29900  fusgrregdegfi  30032  g0wlk0  30113  wlkdlem2  30144  upgrwlkdvdelem  30204  crctcshwlkn0lem3  30283  crctcshwlkn0lem5  30285  wspn0  30395  usgrwwlks2on  30429  umgrwwlks2on  30430  elwspths2spth  30441  clwlkclwwlklem2a  30471  clwlkclwwlklem3  30474  clwwlkn1loopb  30516  clwwlknonwwlknonb  30579  clwwlknonex2lem2  30581  3cyclfrgrrn2  30770  frgrncvvdeqlem8  30789  frgrwopregasn  30799  frgrwopregbsn  30800  frgrwopreg1  30801  frgrwopreg2  30802  frgrregord013  30878  frgrogt3nreg  30880  ablocom  31032  ubthlem1  31354  shaddcl  31701  shmulcl  31702  spansnss2  32059  cnopc  32397  cnfnc  32414  adj1  32417  pjorthcoi  32653  stj  32719  mdsl1i  32805  chirredlem1  32874  mdsymlem5  32891  cdj3lem2b  32921  slmdlema  33646  vonf1oonfo  35715  pconncn  35806  cvmlift2lem1  35884  fmla0xp  35965  ss2mcls  36150  antnestlaw2  36274  dfon2lem6  36368  waj-ax  37036  lukshef-ax2  37037  tr0elw  37106  bj-alrim  37429  bj-nexdt  37433  sucneqond  38122  rdgssun  38135  ptrecube  38372  poimirlem26  38398  poimirlem29  38401  heiborlem1  38564  rngodm1dm2  38685  rngoueqz  38693  zerdivemp1x  38700  isdrngo3  38712  0rngo  38780  pridl  38790  ispridlc  38823  isdmn3  38827  dmnnzd  38828  elrelscnveq3  39378  lshpcmp  39864  omllaw  40119  dochexmidlem7  42342  lspindp5  42646  zdivgd  43215  fsuppind  43439  dfac21  43910  eexinst11  45353  ax6e2eq  45383  e222  45462  e111  45500  e333  45558  imarnf1pr  48173  2ffzoeq  48219  iccpartigtl  48326  iccpartgt  48330  lighneallem3  48513  lighneal  48517  requad1  48541  evenltle  48636  fppr2odd  48650  sgoldbeven3prm  48702  bgoldbtbndlem2  48725  isubgr3stgrlem4  48888  isubgr3stgrlem7  48891  gpgedg2iv  48986  isidom3  49263  idomnzd  49264  lincdifsn  49357  lindslinindimp2lem4  49394  snlindsntor  49404  lincresunit3lem1  49412  lincresunit3lem2  49413  f002  49785  setrec1lem2  50617