Theorem biimpd 135

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 130	. 2 |- ((ps <-> ch) -> (ps -> ch))
3	1, 2	syl 12	1 |- (ph -> (ps -> ch))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  biimpcd 137  mpbii 168  mpbid 170  sylibd 177  sylbid 178  syl5bi 183  syl6bi 187  biimpa 324  bitrd 406  ibi 449  anbi2d 468  elimant 505  mtbird 537  mtbiri 539  consensus 574  del34b 837  chv2 850  a4b1 928  2eu3 1069  ceqsalg 1362  vtoclf 1377  vtocl2 1379  vtocl3 1380  cla4gf 1394  reuuni1 1955  iununi 2037  ordtr2 2257  onint 2261  oneqmin 2273  trsuc 2308  onmindif 2312  ordsucelsuc 2324  limom 2387  findsg 2398  tfinds 2401  tfindsg 2402  tz6.12i 2847  fvelrn 2883  chfnrn 2885  ffnfv 2892  isomin 2937  f1oweOLD 2944  canth 2945  oaordi 3148  oawordri 3152  oaordex 3160  oalimcl 3162  dom2d 3307  nneneq 3408  pssnn 3428  unfilem2 3439  suc11reg 3456  zornlem7 3609  cardlim 3657  alephnbtwn 3674  alephord2i 3682  cardaleph 3690  alephiso 3697  cflim 3704  mulcanpi 3821  genpcd 3903  genpnmax 3904  prlem934a 3931  prlem934b 3932  prlem934 3933  ltexprlem4 3939  reclem4pr 3953  suplem2pr 3956  suppsr2 4017  axltadd 4085  mul0or 4210  divmuldivt 4263  divdivdivt 4265  ltletrt 4290  addgegt0 4325  nn2get 4438  nominpos 4509  elnn0nn 4593  uzind 4603  qbtwnre 4650  cjret 4829  ruclem24 4908  ocin 5177  projlem15 5207  shmods 5363  pjin 5584  pjrn 5587  stadd 5687  stadd3 5689  dmdbr 5731  dmdbr2 5733  atcv1 5768

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

This theorem depends on definitions:  df-bi 128

metamath.org