HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem syl5ib 206
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
StepHypRef Expression
1 syl5ib.1 . 2 |- (ph -> (ps -> ch))
2 syl5ib.2 . . 3 |- (th <-> ps)
32biimp 151 . 2 |- (th -> ps)
41, 3syl5 21 1 |- (ph -> (th -> ch))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146
This theorem is referenced by:  orel2 252  ancomsd 437  pm5.18 658  ccased 754  oplem1 770  3jao 883  19.9t 1031  sbequ2 1175  ax11indn 1359  ax11indi 1360  mo 1386  2mo 1440  necon3ad 1594  necon1ad 1623  r19.23ad 1737  moi 1915  disjsn 2431  pwpw0 2460  prss 2462  sssn 2464  eqsn 2465  tpss 2467  prel12 2475  intss1 2538  intmin 2543  iinss 2590  trel3 2678  trin 2680  ssopab2 2811  po3nr 2839  fri 2908  frirr 2914  fr2nr 2915  fr3nr 2916  dfwe2 2925  wefrc 2933  onfr 2976  ssorduni 2983  ord0eln0 3013  onmindif 3050  onmindif2 3051  ordunel 3074  limuni3 3113  tfis2f 3118  tfinds2 3155  tfinds3 3156  brrelex 3197  brelg 3212  ssrel 3237  relop 3265  funopg 3533  funssres 3538  funun 3540  funcnvuni 3550  fv3 3718  fvelima 3749  eqfnfv 3782  funfvop 3788  dff2 3802  dff3 3803  fopab2 3808  fvclss 3840  cbvfo 3870  isomin 3884  isofrlem 3886  f1oweALT 3891  canth 3892  iunon 3894  iinon 3895  tfrlem1 3896  tfr3 3911  oaordi 4164  oawordeulem 4172  oeordi 4198  oaabs 4236  nneob 4239  omsmolem 4240  erdisj 4270  th3qlem1 4298  mapenlem2 4470  mapdom2 4474  phplem4 4491  php3 4495  fiint 4534  fodomfi 4540  iunfi 4543  suppr 4562  elirrv 4570  suc11reg 4577  trcl 4617  zfregs 4619  rankxplim3 4686  cplem1 4692  karden 4698  aceq3lem 4704  aceq5 4712  aceq6b 4714  ac6lem 4726  zorn2lem4 4763  zorn2lem5 4764  zorn2lem7 4766  brdom6disj 4777  fnrndomg 4779  unidom 4780  carddom 4808  unxpdomlem 4815  alephordi 4846  alephord 4847  alephval2 4874  cfub 4880  ltmpi 5003  ltexpq 5052  ltexprlem2 5115  ltexprlem6 5119  reclem3pr 5130  reclem4pr 5131  suplem1pr 5133  mulgt0sr 5186  ssgt0sr 5189  suppsrlem 5193  suppsr2 5195  suppsr3 5196  supsr 5203  suprelem 5231  axrrecex 5256  pre-axsup 5263  ltlent 5495  nnleltp1t 5901  infmrcl 6016  xrsupexmnf 6021  xrinfmexpnf 6022  xrsupsslem 6023  xrinfmsslem 6024  xrub 6027  supxrre 6030  supxrun 6032  lt0nnn0 6063  nnnn0addclt 6072  elnn0nn 6118  flval3t 6182  fznt 6425  expp1t 6506  expne0it 6519  expge0t 6522  nn0opth 6596  creur 6673  creui 6674  seq1bnd 6847  seq1ublem 6848  cau3i 6851  cau5i 6854  cau4i 6855  cau5 6856  facwordit 6881  faclbnd4lem4 6888  bccl2t 6909  2climnn 7039  2climnn0 7040  climaddlem3 7052  climmullem8 7063  climsup 7091  ser1f0 7106  cvgcmp3cetlem2 7125  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  acdc2 7432  acdc 7437  infxpidmlem7 7501  infxpidmlem8 7502  infxpidmlem12 7506  infdif 7511  unctb 7519  unitgt 7565  tgclt 7566  bastop 7584  subtop 7588  indistop 7590  fctop 7592  cctop 7594  elcls3 7652  cnsscnp 7711  cncnp 7717  cnconst 7719  sncld 7726  opnuni 7808  iscau3 7876  xpcn 7910  iscms2lem5 7927  bcthlem8 7940  bcthlem33 7965  ghgrpilem2 8071  nmoubi 8367  spwval2 8577  shftefif1olem 8661  shftefif1olemOLD 8662  chcmh 9034  occllem6 9094  pjtheu 9150  shmods 9277  spanunsn 9419  h1datom 9421  osumlem7 9501  nmopubt 9749  nmfnleubt 9765  stm1r 10081  mdsl1 10156  cvmd 10159  superpos 10189  chjatom 10192  irred 10229  atcvat4 10232  sumdmdi 10249  sumdmdlem 10252  cdj3lem2a 10268  cdj3lem3a 10271  cdj3 10273  uninqs 10342  cdrci 10381  bsi 10382  mapudiscn 10399  qusp 10430  oefil2 10441  fisub 10447
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 147
Copyright terms: Public domain