Theorem biimprcd 173

Description: Deduce a converse commuted implication from a logical equivalence.

Hypothesis

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

Assertion

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

Proof of Theorem biimprcd

Step	Hyp	Ref	Expression
1		biimpd.1	. . 3 |- (ph -> (ps <-> ch))
2	1	biimprd 171	. 2 |- (ph -> (ch -> ps))
3	2	com12 14	1 |- (ch -> (ph -> ps))

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

This theorem is referenced by:  biimparc 463  prlem1OLD 849  ax11i 1498  ax11eq 1754  ax11el 1755  eleq1a 1966  ceqsalg 2314  ceqsalgOLD 2315  cgsexg 2321  cgsex2g 2322  cgsex4g 2323  ceqsex 2324  cla42egv 2366  cla43egv 2368  dfiin2g 3286  onfr 3702  ordun 3771  ralxfr 3839  iunpw 3858  ssrel 4075  ssrelrel 4083  iss 4254  funcnvuni 4482  funfvop 4776  cbvfo 4861  abianfp 5171  oaordex 5240  eceqopreq 5372  fundmen 5487  nneneq 5606  unfilem1 5641  ordtypelem3 5686  tratrb 5831  omsublim 5887  ac6lem 5916  zorn2lem3 5952  zorn2lem7 5956  ltrpq 6237  genpnnp 6260  ltaddpr 6292  reclem3pr 6310  reclem4pr 6311  suppsrlem 6373  suppsr3 6376  suprelem 6411  elfz4 7645  fzsuc 7678  abslti 8127  abslei 8128  cau2i 8165  fsum1i 8265  ser1clim0 8433  unctb 8846  txbas 8933  txuni 8935  cnsscnp 9049  nmoubi 9774  dif1en 10172  uptx 10226  txcnopab 10228  ismnd2 10392  grpmnd 10393  nmopub 11469  nmfnleub 11486  mdbr3 11869  mdbr4 11870  atssma 11950  atcvatlem 11957  gcdcllem2 13719  gcdcllem3 13720  isprm2lem 13774  nepss 13820  ordsucuniel 13863  nodmon 13994  axdenselem4 14022  nocvxminlem 14028  uninqs 14340  prl2 14514  nfwpr4c 14630  fprod1i 14673  hmphre 14884  iintlem1 15010  cnvtr 15016  mrdmcd 15143  elincin 15220  isline1 15294  dfiin2gOLD 15356  ordtypelem3OLD 15377  omsublimOLD 15396  hscptsscld 15434  alexsublem2 15438  fbasfip 15556  fimax 15746  indexdom 15754  sdc 15811  fdc 15812  fsumlt1 15831  txsubsp 15912  heiborlem1 15955  heiborlem28 15982  ceqsex3OLD 16249  pm13.14 16370  smores 16446  3impexpbicomVD 16681  hbra2VD 16684  tratrbVD 16685  equncomVD 16692  trsbcVD 16701  lubun 16899  lubunNEW 16900  ispsubcl2 17356

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 164

Copyright terms: Public domain