Theorem syl5cbir 228

Description: A mixed syllogism inference.

Hypotheses

Ref	Expression
syl5bir.1	|- (ph -> (ps <-> ch))
syl5bir.2	|- (th -> ch)

Assertion

Ref	Expression
syl5cbir	|- (th -> (ph -> ps))

Proof of Theorem syl5cbir

Step	Hyp	Ref	Expression
1		syl5bir.1	. . 3 |- (ph -> (ps <-> ch))
2		syl5bir.2	. . 3 |- (th -> ch)
3	1, 2	syl5bir 227	. 2 |- (ph -> (th -> ps))
4	3	com12 14	1 |- (th -> (ph -> ps))

Syntax hints:   -> wi 3   <-> wb 163

This theorem is referenced by:  elsnc2g 3070  fr2nr 3635  tz7.2 3639  ordtri1 3693  ordtri1OLD 3694  reuuni1 3808  eualeqhb 3824  euexeqOLD 3826  eufromeq2 3829  eufromeq6 3833  reuhypd 3848  fr3nr 3859  oneqmin 3886  nlimsucg 3923  nlimsucgOLD 3924  onzsl 3928  tfinds 3942  opelxpex2 4119  opelxpex2OLD 4120  funcnvuni 4482  fsn 4807  fconst2g 4821  funfvima 4828  ndmoprcl 4977  omordi 5245  omord 5247  omwordi 5250  omsmolem 5313  pw2en 5505  pwne 5552  2pwne 5553  php 5607  pwfi 5661  suppr 5680  suc11reg 5710  inf3lemd 5718  en3lplem1 5756  tz9.12lem1 5770  aceq5 5902  isinfcard 6035  addnidpi 6180  distrlem5pr 6283  cnegex 6502  xrmax1 7092  xrmin2 7095  max1ALT 7099  nnleltp1 7138  sup2 7260  xrsupexmnf 7283  xrinfmexpnf 7284  xrub 7289  nnnn0addcl 7334  nn0sub 7370  zltp1le 7390  qre 7439  elfzp1 7683  fzsn 7684  fz1sbc 7696  fsequb 7702  expp1 7817  expge0 7833  sqrlem18 7940  seq1bndi 8162  reccnv 8479  infcvgaux1i 8480  expcnv 8494  elcncf1di 8532  infxpidmlem10 8830  txbas 8933  gapm 9462  nvmul0or 9604  ipasslem5 9835  ipasslem11 9841  minveclem10 9899  efifolem5 10080  circgrp 10094  upxp 10225  uptx 10226  subspid 10249  stoig 10251  filintf 10274  fgfil 10290  extbas1 10291  filrn 10293  filmapss 10309  hvmul0or 10526  his6 10598  ocsh 10789  ocin 10802  projlem8 10826  shsleji 10971  shsidmi 10990  chnlen0 11001  h1de2bi 11110  h1de2ctlem 11111  h1de2ci 11112  osumlem1 11213  3oalem1 11242  atcveq0 11920  chcv1 11927  cdjreui 12004  cdj3lem2b 12009  bnj144 12476  eucalginv 13752  eucalglt 13753  coprm 13782  untsucf 13798  ordsucuniel 13863  wfrlem14 13970  wfrlem15 13971  axfelem15 14045  axfelem16 14046  f1fi 14377  repcpwti 14503  nZdef 14527  fincmpzer 14711  fprodsub 14742  trran2 14757  intfmu2 14867  homcard 14893  eqindhome 14895  cntrsetlem 14999  trran 15014  cptarc 15242  vtarsuelt 15272  partarelt1 15273  elicc3 15362  ccid 15363  elfiun 15369  opncldf1 15402  opnregcld 15415  cldregopn 15416  subcls 15424  subntr 15425  hscptsscld 15434  alexsublem3 15439  alexsublem4 15440  connsub 15443  cnconn 15444  comppfsc 15517  neibastop2lem4 15522  fnejoin2 15531  filfinnfr 15561  isufil2 15565  filssufillem 15570  filssufil 15571  ufileulem 15572  ufileu 15573  filufint 15574  ufilen 15579  filcon 15580  flimcls 15588  rnelfm 15593  fmfnfmlem1 15594  fmfnfm 15598  flimfcls 15613  flimfnfcls 15615  fcluscnplem 15617  fcluscomplem 15620  fcluscomp 15621  filnetlem1 15640  filnetlem4 15643  filnet 15645  unirep 15664  foco2 15686  cocanfo 15689  upixp 15729  eropreu 15733  eroprf 15735  frfi 15771  elfzp12 15795  fzm1 15796  absmod0 15802  sdc 15811  fsum00 15820  fsumlt1 15831  subspcld2 15839  mettrifi 15847  oprpiece1res2 15881  cnimass 15888  cnresima 15891  txsubsp 15912  txmet 15925  sstotbnd 15936  totbndbnd 15944  heiborlem1 15955  heiborlem29 15983  rrntotbnd 16022  grpeqdivid 16038  phtpycolem5 16055  pi1gp 16095  isdivrng3 16112  crnghomfo 16154  0idl 16173  1idl 16174  divrngidl 16176  smprngpr 16200  prnc 16215  ispridlc 16218  pm14.24 16397  addrcom 16475  glb0 16920  cmtbr4 16976  cvrnbtwn2 16992  cvrnbtwn4 16996  atomcvreq0 17010  atomnlej1 17030  atomnlej2 17031  hlatexch1 17045  ps2 17079  pmapglb2 17253  pmapglb2x 17254  paddasslem17 17297

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164

Copyright terms: Public domain