Theorem syl5ib 223

Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition.

Hypotheses

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

Assertion

Ref	Expression
syl5ib	|- (ph -> (th -> ch))

Proof of Theorem syl5ib

Step	Hyp	Ref	Expression
1		syl5ib.1	. 2 |- (ph -> (ps -> ch))
2		syl5ib.2	. . 3 |- (th <-> ps)
3	2	biimpi 168	. 2 |- (th -> ps)
4	1, 3	syl5 20	1 |- (ph -> (th -> ch))

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

This theorem is referenced by:  orel2 272  ancomsd 485  pm5.18OLD 723  ccased 830  oplem1 852  dn1OLD 856  3jao 1158  3jaaoOLD 1165  3impexp 1286  19.9t 1382  sbequ2 1543  ax11indn 1757  mo 1787  2euex 1844  2mo 1851  necon3adOLD 2038  necon3bd 2039  necon2ad 2055  necon1ad 2079  pm2.61dne 2091  r19.23adOLD 2214  rcla4 2373  moi2 2435  moi 2436  euind 2439  reuind 2450  disjsnOLD 3090  pwpw0 3134  prssOLD 3139  sssn 3142  eqsn 3143  tpssOLD 3146  prel12 3155  pwsnALT 3173  intss1 3231  intmin 3237  intminOLD 3238  uniintsn 3253  iinss 3304  iinssOLD 3305  trel3 3420  trin 3422  trintss 3427  copsexg 3537  ssopab2 3573  po3nr 3600  fri 3626  frirr 3634  fr2nr 3635  wefrc 3652  onfr 3702  ord0eln0 3717  trsuc2 3754  onmindif 3760  fr3nr 3859  dfwe2OLD 3862  ssorduni 3870  ssorduniOLD 3871  onmindif2 3893  ordunel 3906  limuni3 3936  tfis2f 3939  tfinds 3942  tfinds2 3947  tfinds3 3948  brrelex 4028  brelg 4047  ssrelOLD 4076  ssrelrel 4083  ssrelrelOLD 4084  relop 4113  iss 4254  asymref2 4310  xpcan 4348  xpcan2 4350  funopg 4454  funssres 4460  funun 4462  funcnvuni 4482  fv3 4690  fvelima 4723  fvelimaOLD 4724  eqfnfv 4766  funfvop 4776  dff3 4790  dff4 4791  fopab2 4796  fvclss 4831  cbvfo 4861  isomin 4876  isofrlem 4878  f1oweALT 4883  canth 5112  iunon 5114  iinon 5115  onfununi 5116  tfrlem1 5119  tfr3 5134  oaordi 5227  oawordeulem 5236  oeordi 5262  oaabs 5309  nneob 5312  omsmolem 5313  erdisj 5344  th3qlem1 5373  ac6sfilem3 5508  ac6sfi 5509  mapenlem2 5584  mapdom2 5588  phplem4 5605  php3 5609  fiint 5650  fodomfi 5656  iunfi 5659  suppr 5680  ordtypelem4 5687  ordtypelem5 5688  ordtypelem6 5689  ordtypelem7 5690  ordtype 5691  hartog 5693  elirrv 5700  suc11reg 5710  trcl 5752  zfregs 5754  rankxplim3 5825  cplem1 5850  karden 5856  elomsubsd 5885  omsublim 5887  infenomsub 5889  omsubinit 5890  aceq3lem 5894  aceq5 5902  aceq6b 5904  ac6lem 5916  zorn2lem4 5953  zorn2lem5 5954  zorn2lem7 5956  brdom6disj 5967  fnrndomg 5969  unidom 5970  carddom 5987  unxpdomlem 5995  alephordi 6022  alephord 6023  alephval2 6050  cfub 6056  ltmpi 6183  ltexpq 6232  ltexprlem2 6295  ltexprlem6 6299  reclem3pr 6310  reclem4pr 6311  suplem1pr 6313  mulgt0sr 6366  ssgt0sr 6369  suppsrlem 6373  suppsr2 6375  suppsr3 6376  supsr 6383  suprelem 6411  axrrecex 6437  pre-axsup 6444  ltlen 6692  nnleltp1 7138  infmrcl 7278  xrsupexmnf 7283  xrinfmexpnf 7284  xrsupsslem 7285  xrinfmsslem 7286  xrub 7289  supxrre 7292  supxrun 7294  lt0nnn0 7325  nnnn0addcl 7334  elnn0nn 7380  flval3 7479  modirr 7522  ioojoin 7585  fzn 7663  expp1 7817  expge0 7833  creur 7992  creui 7993  seq1bndi 8162  seq1ublem 8163  cau3ii 8166  cau5ii 8169  cau4ii 8170  cau5i 8171  facwordi 8196  faclbnd4lem4 8203  bccl2 8223  2climnn 8362  2climnn0 8363  climaddlem3 8376  climmullem8 8387  climsupi 8415  cvgcmp3cetlem2 8450  ivthlem6 8548  ivthlem7 8549  acdc2 8759  acdc 8764  infxpidmlem7 8827  infxpidmlem8 8828  infxpidmlem12 8832  infdif 8837  unctb 8846  unitg 8893  tgcl 8894  bastop1 8912  subtop 8916  indistop 8918  fctop 8920  cctop 8922  txbas 8933  txuni 8935  elcls3 8987  cnsscnp 9049  cncnp 9055  cnconst 9057  sncld 9064  opnuni 9145  iscau3 9216  iscau4 9218  xpcn 9254  iscms2lem5 9271  bcthlem8 9284  bcthlem33 9309  gxnn0neg 9386  gxnn0suc 9387  ghgrpilem2 9442  ssga 9455  gapmlem 9461  nmoubi 9774  lnon0 9798  spwval2 9996  shftefif1olem 10095  indexfi 10174  fipreima 10175  ficard 10176  fixp 10180  cdrci 10182  fiuni 10219  subtopmet 10256  oefil2 10275  fbssint 10279  fbunfip 10282  fgbas 10286  extbas1 10291  filrn 10293  hausfillim 10303  filmapss 10309  elfilmap 10312  cncomp 10331  on1el3 10412  chcmhi 10746  occllem6 10811  pjtheui 10868  shmodsi 10995  spanunsni 11135  h1datomi 11137  osumlem7 11219  nmopub 11469  nmfnleub 11486  stm1ri 11816  stadd3i 11820  mdsl1i 11893  cvmdi 11896  superpos 11926  chjatom 11929  irredi 11966  atcvat4i 11969  sumdmdii 11987  sumdmdlem 11990  cdj3lem2a 12008  cdj3lem3a 12011  cdj3i 12013  bnj1114 13419  negn0 13655  lbzbi 13657  gcdcllem2 13719  gcdcllem3 13720  gcd0id 13729  algcvgblem 13745  eucalglt 13753  trsuc2OLD 13793  trintssOLD 13795  untsucf 13798  3orel1 13805  3orel2 13806  3orel3 13807  nepss 13820  dfon2lem5 13853  dfon2lem6 13854  dfon2lem7 13855  dfon2lem8 13856  ordsucuniel 13863  tz6.26 13913  wfi 13915  wfis2fg 13919  trcltr 13936  frmin 13938  frind 13939  frins2fg 13943  poxp 13949  soxp 13950  wfrlem14 13970  wfrlem15 13971  axdenselem4 14022  axdenselem8 14026  nocvxmin 14029  axfelem14 14044  axfelem15 14045  axfelem16 14046  arg-ax 14240  uninqs 14340  domrngref 14364  restidsing 14391  inpreima5 14469  fopab2g 14485  prjmapcp 14507  nZdef 14527  inposet 14620  bsi 14845  mapudiscn 14872  sallnei 14873  nsn 14874  osneisi 14875  qusp 14908  fisub 14924  rcfpfillem4 14931  rcfpfillem6 14933  conttnf 14944  bwt2 14960  supbrr 15048  trer 15361  elicc3 15362  ioodisj 15364  finminlem 15367  elfiun 15369  fictb 15371  inficlALT 15372  finsschain 15373  ordtypelem4OLD 15378  ordtypelem5OLD 15379  ordtypelem6OLD 15380  ordtypelem7OLD 15381  ordtypeOLD 15382  hartogOLD 15384  elomsubsdOLD 15394  omsublimOLD 15396  infenomsubOLD 15398  omsubinitOLD 15399  opncldf1 15402  opnnei 15417  subntr 15425  compsublem 15430  compsub 15431  cptclsscpt 15432  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem1 15437  alexsublem2 15438  alexsublem3 15439  alexsublem4 15440  alexsub 15441  cnconn 15444  reconnlem1 15446  reconnlem5 15450  2ndcctbss 15478  fneint 15486  fnessref 15503  refssfne 15504  locfincomp 15514  comppfsc 15517  neibastop1 15518  neibastop2lem1 15519  neibastop2lem2 15520  neibastop2lem4 15522  neibastop3 15524  topmeet 15526  topjoin 15527  fnemeet1 15528  fnemeet2 15529  fnejoin1 15530  fnejoin2 15531  ist1-3 15543  opnfbas 15557  neifg 15559  supfil 15560  isufil2 15565  filssufillem 15570  filssufil 15571  ufileu 15573  filufint 15574  uffixfr 15575  fixufil 15576  ufinffr 15578  ufilen 15579  filcon 15580  ufcondr 15581  cnpfillim 15589  rnelfmlem 15592  rnelfm 15593  fmfnfmlem2 15595  fmfnfmlem3 15596  fmfnfmlem4 15597  fmfnfm 15598  flimfbas 15601  sfcls 15604  filclus 15605  fcluscnplem 15617  fcluscomplem 15620  fcluscomp 15621  tailfb 15639  filnetlem4 15643  filnetlem5 15644  filnet 15645  ralunOLD 15657  unirep 15664  prfunOLD 15677  eropreu 15733  eroprf 15735  findcard2 15745  indexfiOLD 15755  fipreimaOLD 15756  inficl 15757  fimax2g 15769  frfi 15771  filbcmb 15776  fzadd2 15791  fzdisj 15793  sdc 15811  fdc 15812  nninfnub 15819  blhalf 15846  haustlmu 15906  txmet 15925  sstotbnd 15936  isbnd3 15941  totbndbnd 15944  heiborlem1 15955  heiborlem32 15986  bfp 16009  rrntotbnd 16022  phtpcdm 16061  phtpcer 16062  pcohtpylem3 16082  0idl 16173  intidl 16177  unichnidl 16179  keridl 16180  prnc 16215  ceqsex3OLD 16249  erreft 16259  prtlem10 16265  prtlem17 16278  prtlem18 16279  prter2 16285  cla4gft 16406  smores 16446  smoiun 16452  snssiALT 16651  lubun 16899  lubunNEW 16900  glbconx 17029  cvrat4 17076  paddasslem17 17297  pmodlem2 17308  poml4 17361  osumcllem8 17371  pexmidlem5 17382

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