Theorem biimprd 154

Description: Deduce a converse implication from a logical equivalence.

Hypothesis

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

Assertion

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

Proof of Theorem biimprd

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

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

This theorem is referenced by:  biimprcd 156  mpbiri 194  mpbird 196  sylibrd 204  sylbird 205  syl5bir 210  syl6bir 215  biimpar 417  bitrd 526  anbi2d 614  mtbid 712  mtbii 714  dral1 1150  sb9i 1258  ax16i 1265  a4eiv 1269  a16g 1271  elabgt 1886  sspsstr 2141  axsep2 2694  so 2855  rabsnt 2884  ralxfrd 2887  dfwe2 2925  wefrc 2933  ordsseleq 2966  oneqmini 3007  ordsssuc2 3049  ordsucelsuc 3063  ordunel 3074  orduniorsuc 3077  ordzsl 3106  tfinds 3151  opelxpi 3207  2elresin 3584  tz6.12c 3725  fveqres 3734  dffo4 3805  fconst5 3833  f1owe 3890  f1oweALT 3891  tfrlem9 3904  tz7.48lem 3940  abianfp 3947  ndmordi 4037  oawordeulem 4172  om00 4190  omlimcl 4193  odi 4194  f1oen2g 4375  f1domg 4377  sbthlem1 4427  fiint 4534  inf3lem3 4587  trcl 4617  r1tr 4626  rankr1 4646  brdom6disj 4777  unidom 4780  entri 4811  cardaleph 4857  indpi 5006  prlem934a 5109  addcanpr 5124  reclem3pr 5130  lttri4t 5487  lelttrt 5496  xrlttrit 5525  xrlelttrt 5535  add20 5576  nnmulclt 5889  lbreu 5992  arch 6018  supxrre 6030  nnnegz 6085  zeot 6146  dfuz 6150  uzwo5OLD 6159  zmax 6168  ioossicc 6330  icoshft 6341  expordt 6533  sqrlem6 6608  absrpclt 6790  nn0absclt 6816  bcclt 6910  climmulc2 7065  iserzcmp0 7079  caucvglem5 7097  reccnv 7153  rescncf 7207  mulc1cncf 7214  infpnlem1 7449  ntrval 7618  cncnplem4 7716  metcnss 7837  metcnss2 7838  dscmet 7856  iscms2lem3 7925  cmsss 7931  sm1cnilem 8281  blocn2 8399  efifolem5 8641  shftefif1olem 8661  shftefif1olemOLD 8662  eff1i 8665  hlim0 9026  projlem15 9116  spanun 9382  spansncol 9407  spansneleq 9409  spansneleqOLD 9410  spansnsst 9411  elspansn5t 9414  0cnop 9819  0cnfn 9820  idcnop 9821  lnopcon 9878  lnfncon 9905  pjnormss 10007  dmdmdt 10137  mdslmd1lem1 10160  mdslmd1lem2 10161  elghomlem2 10288  ghomgsg 10300  ghomf1olem 10301  cayleylem2 10317  ompfl2OLD 10327  uninqs 10342  fiv 10374  mapdiscn 10398  cnvhmphb 10413  efilcp2 10450

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