Theorem biimpd 153

Description: Deduce an implication from a logical equivalence.

Hypothesis

Ref	Expression
biimpd.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
biimpd	|- (ph -> (ps -> ch))

Proof of Theorem biimpd

Step	Hyp	Ref	Expression
1		biimpd.1	. 2 |- (ph -> (ps <-> ch))
2		bi1 148	. 2 |- ((ps <-> ch) -> (ps -> ch))
3	1, 2	syl 10	1 |- (ph -> (ps -> ch))

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

This theorem is referenced by:  biimpcd 155  mpbii 193  mpbid 195  sylibd 202  sylbid 203  syl5bi 208  syl6bi 214  biimpa 416  bitrd 526  ibi 590  anbi2d 614  mtbird 713  mtbiri 715  consensus 765  dral1 1150  chvar 1163  sbequi 1223  a4v 1267  2eu3 1444  ceqsalg 1816  vtoclf 1832  vtocl2 1834  vtocl3 1835  cla4gf 1851  ra4sbc 1987  iununi 2606  reuuni1 2872  elpwunsn 2902  ordtr2 2992  onint 2996  oneqmin 3008  trsuc 3045  ordsssuc2 3049  onmindif 3050  ordsucelsuc 3063  ordunisuc2 3105  limom 3136  findsg 3147  tfinds 3151  tfindsg 3152  relop 3265  unixp0 3504  tz6.12i 3726  chfnrn 3787  exfo 3807  ffnfv 3813  funiunfv 3851  isomin 3884  f1oweALT 3891  canth 3892  oaordi 4164  oawordri 4168  oaordex 4176  oalimcl 4178  oarec 4180  omwordi 4186  oewordi 4202  oelim2 4206  dom2d 4385  nneneq 4492  pssnn 4513  unfilem2 4525  suc11reg 4577  zorn2lem7 4766  unidom 4780  uniimadom 4782  cardlim 4823  alephnbtwn 4840  alephord2i 4849  cardaleph 4857  alephiso 4864  cflim 4881  mulcanpi 4999  genpcd 5081  genpnmax 5082  prlem934a 5109  prlem934b 5110  prlem934 5111  ltexprlem4 5117  reclem4pr 5131  suplem2pr 5134  suppsr2 5195  pre-axltadd 5261  ltletrt 5497  xrltletrt 5536  addgegt0 5574  mul0or 5663  divne0t 5692  divmuldivt 5736  divdivdivt 5741  prodgt02t 5783  prodge02t 5785  lemul1it 5793  lemul1itOLD 5794  mulgt1t 5801  divgt0t 5809  divge0t 5810  ledivp1 5854  ltdivp1 5855  nominpos 5990  supxr 6028  elnn0nn 6118  btwnnzt 6139  dfuz 6150  uzindOLD 6156  zmax 6168  flval2t 6181  flval3t 6182  qbtwnre 6216  iccsupr 6331  icoshft 6341  icoshftf1oi 6342  fsequb2 6456  fseqsupcl 6457  fseqsupub 6458  expne0it 6519  expwordit 6534  expword2it 6536  sq01t 6582  cjret 6745  seq1ublem 6848  cvg1 6858  bccl2t 6909  climaddc2 7055  climsqueeze 7076  climsqueeze2 7077  expcnvlem6 7167  georeclim 7175  cvgratlem1ALT 7182  cvgratlem1 7185  cncffvelrnOLD 7202  mulc1cncf 7214  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  efcltlem1 7246  reeff1 7350  reeff1o 7368  ruclem24 7476  bastop 7584  clsval2 7627  0ntr 7644  islpi 7690  cnpco 7708  cncnplem2 7714  cncnplem4 7716  sncld 7726  metxp 7774  caussi 7889  metelcls 7900  metcn4i 7906  xplmi 7907  xpcn 7910  lmcau 7930  bcthlem16 7948  grplactf1o 8034  issubg 8053  nvlmle 8268  hlipgt0 8546  efif1lem3 8647  ocin 9085  ocnelt 9086  projlem15 9116  shmods 9277  pjmf1 9578  unopf1ot 9756  stadd 10083  stadd3 10085  mdit 10132  dmdmdt 10137  dmdit 10139  dmdbr2 10140  dmdbr3 10141  dmdbr4 10142  dmdi4 10143  mdsl1 10156  superpos 10189  cvbr3 10202  atssmat 10213  atcv1t 10215  atoml 10217  irredlem1 10225  elghomlem2 10288  ompfl2OLD 10327  uninqs 10342  fiiu 10350  ficli 10368  fiiu2 10377  cdrci 10381  bsi 10382  truni1 10386  cnrsfin 10396  cnrscoa 10397  mapdiscn 10398  cnvhmphb 10413  hmphsyma 10415  hmphtr 10418  homcard 10426  fillsb 10435  filint 10437  infi 10448  cnfilca 10451  dmse1 10467  ltsubpostb 10471  ltaddpos2tb 10472  iintlem1 10476  rdmob 10525  eqidob 10567  ismonc 10584  cmpmon 10585  idmon 10588

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