Theorem syl5ib 204

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 149	. 2 |- (th -> ps)
4	1, 3	syl5 21	1 |- (ph -> (th -> ch))

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

This theorem is referenced by:  orel2 250  ancomsd 439  pm5.18 663  ccased 761  oplem1 777  dn1 779  3jao 892  19.9t 1071  sbequ2 1216  ax11indn 1405  ax11indi 1406  mo 1432  2mo 1487  necon3ad 1645  necon1ad 1675  r19.23ad 1791  moi2 1970  moi 1971  disjsn 2502  pwpw0 2533  prss 2536  sssn 2538  eqsn 2539  tpss 2541  prel12 2549  pwsnALT 2566  intss1 2615  intmin 2620  iinss 2668  trel3 2762  trin 2764  ssopab2 2900  po3nr 2926  fri 2948  frirr 2954  fr2nr 2955  wefrc 2970  onfr 3014  ord0eln0 3027  onmindif 3061  fr3nr 3138  dfwe2 3140  ssorduni 3147  onmindif2 3169  ordunel 3181  limuni3 3206  tfis2f 3209  tfinds2 3216  tfinds3 3217  brrelex 3290  brelg 3307  ssrel 3334  ssrelrel 3340  relop 3365  funopg 3652  funssres 3657  funun 3659  funcnvuni 3669  fv3 3844  fvelima 3875  eqfnfv 3909  eqfnfv2 3911  funfvop 3917  dff3 3931  dff4 3932  fopab2 3937  fvclss 3969  cbvfo 3999  isomin 4013  isofrlem 4015  f1oweALT 4020  canth 4205  iunon 4207  iinon 4208  onfununi 4209  tfrlem1 4212  tfr3 4227  oaordi 4316  oawordeulem 4324  oeordi 4350  oaabs 4392  nneob 4395  omsmolem 4396  erdisj 4426  th3qlem1 4455  ac6sfilem3 4590  ac6sfi 4591  mapenlem2 4637  mapdom2 4641  phplem4 4658  php3 4662  fiint 4703  fodomfi 4709  iunfi 4712  suppr 4733  elirrv 4741  suc11reg 4750  trcl 4791  zfregs 4793  rankxplim3 4860  cplem1 4866  karden 4872  aceq3lem 4878  aceq5 4886  aceq6b 4888  ac6lem 4900  zorn2lem4 4937  zorn2lem5 4938  zorn2lem7 4940  brdom6disj 4951  fnrndomg 4953  unidom 4954  carddom 4985  unxpdomlem 4993  alephordi 5024  alephord 5025  alephval2 5052  cfub 5058  ltmpi 5185  ltexpq 5234  ltexprlem2 5297  ltexprlem6 5301  reclem3pr 5312  reclem4pr 5313  suplem1pr 5315  mulgt0sr 5368  ssgt0sr 5371  suppsrlem 5375  suppsr2 5377  suppsr3 5378  supsr 5385  suprelem 5413  axrrecex 5438  pre-axsup 5445  ltlen 5676  nnleltp1 6100  infmrcl 6237  xrsupexmnf 6242  xrinfmexpnf 6243  xrsupsslem 6244  xrinfmsslem 6245  xrub 6248  supxrre 6251  supxrun 6253  lt0nnn0 6284  nnnn0addcl 6293  elnn0nn 6339  flval3 6438  modirr 6481  ioojoin 6543  fzn 6621  expp1 6769  expge0 6785  nn0opthi 6867  creur 6943  creui 6944  seq1bndi 7113  seq1ublem 7114  cau3ii 7117  cau5ii 7120  cau4ii 7121  cau5i 7122  facwordi 7147  faclbnd4lem4 7154  bccl2 7174  2climnn 7305  2climnn0 7306  climaddlem3 7319  climmullem8 7330  climsupi 7358  cvgcmp3cetlem2 7393  ivthlem6 7491  ivthlem7 7492  acdc2 7702  acdc 7707  infxpidmlem7 7770  infxpidmlem8 7771  infxpidmlem12 7775  infdif 7780  unctb 7789  unitg 7835  tgcl 7836  bastop1 7854  subtop 7858  indistop 7860  cctop 7862  elcls3 7921  cnsscnp 7982  cncnp 7988  cnconst 7990  sncld 7997  opnuni 8078  iscau3 8149  iscau4 8151  xpcn 8187  iscms2lem5 8204  bcthlem8 8217  bcthlem33 8242  gxnn0neg 8319  gxnn0suc 8320  ghgrpilem2 8375  nmoubi 8689  lnon0 8713  spwval2 8915  shftefif1olem 9013  chcmhi 9389  occllem6 9454  pjtheui 9511  shmodsi 9638  spanunsni 9778  h1datomi 9780  osumlem7 9862  nmopub 10112  nmfnleub 10129  stm1ri 10452  stadd3i 10456  mdsl1i 10529  cvmdi 10532  superpos 10562  chjatom 10565  irredi 10603  atcvat4i 10606  sumdmdii 10624  sumdmdlem 10627  cdj3lem2a 10645  cdj3lem3a 10648  cdj3i 10650  uninqs 10730  domrngref 10764  restidsing 10805  inposet 10868  on1el3 10962  cdrci 10994  bsi 10995  mapudiscn 11015  sallnei 11016  nsn 11017  osneisi 11018  qusp 11068  oefil2 11079  fisub 11085  rcfpfillem4 11092  rcfpfillem6 11094  bwt2 11123  3jaao 11388  xpss1 11403  xpss2 11404  trer 11409  elicc3 11410  ioodisj 11413  finminlem 11418  fiuni 11420  elfiun 11421  fictb 11423  inficlALT 11424  finsschain 11425  ordtypelem4 11430  ordtypelem5 11431  ordtypelem6 11432  ordtypelem7 11433  ordtype 11434  hartog 11436  elomsubsd 11446  omsublim 11448  infenomsub 11450  omsubinit 11451  opncldf1 11454  opnnei 11469  subntr 11482  compsublem 11487  compsub 11488  cptclsscpt 11489  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem1 11496  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  alexsub 11500  cnconn 11503  subtopmet 11506  reconnlem1 11507  reconnlem5 11511  2ndcctbss 11539  fneint 11547  fnessref 11564  refssfne 11565  locfincomp 11575  comppfsc 11578  neibastop1 11579  neibastop2lem1 11580  neibastop2lem2 11581  neibastop2lem4 11583  neibastop3 11585  topmeet 11587  topjoin 11588  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  fnejoin2 11592  ist1-3 11604  fbssint 11626  opnfbas 11629  fbunfip 11631  fgbas 11636  extbas1 11641  filrn 11643  neifg 11644  supfil 11645  isufil2 11650  filssufillem 11655  filssufil 11656  ufileu 11658  filufint 11659  uffixfr 11660  fixufil 11661  ufinffr 11663  ufilen 11664  filcon 11665  ufcondr 11666  hausfillim 11685  cnpfillim 11686  elfilmap 11690  filmapss 11696  rnelfmlem 11698  rnelfm 11699  fmfnfmlem2 11701  fmfnfmlem3 11702  fmfnfmlem4 11703  fmfnfm 11704  flimfbas 11713  sfcls 11716  filclus 11717  fcluscnplem 11729  fcluscomplem 11732  fcluscomp 11733  tailfb 11762  filnetlem4 11766  filnetlem5 11767  filnet 11768  ssga 11777  gapmlem 11783  ralun 11789  ficard 11834  fixp 11840  indexf 11847  fipreima 11848  inficl 11849  filbcmb 11857  sdc 11877  nninfnub 11882  metsstop 11909  blhalf 11911  haustlmu 11967  txbas 11973  txuni 11975  sstotbnd 11992  isbnd3 11997  totbndbnd 12000  heiborlem1 12011  heiborlem32 12042  bfp 12065  rrntotbnd 12078  phtpcdm 12103  phtpcer 12104

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 145

Copyright terms: Public domain