Theorem biimprcd 156

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 154	. 2 |- (ph -> (ch -> ps))
3	2	com12 11	1 |- (ch -> (ph -> ps))

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

This theorem is referenced by:  biimparc 419  prlem1 770  ax11i 1138  ax11eq 1363  ax11el 1364  eleq1a 1543  ceqsalg 1825  cgsexg 1831  cgsex2g 1832  cgsex4g 1833  ceqsex 1834  cla42egv 1864  cla43egv 1866  ralxfr 2899  iunpw 2914  onfr 2986  ordun 3081  funcnvuni 3564  funfvop 3803  cbvfo 3885  abianfp 3962  oaordex 4192  ecelqsi 4292  eceqopreq 4313  fundmen 4428  nneneq 4512  unfilem1 4548  ac6lem 4754  zorn2lem3 4790  zorn2lem7 4794  ltrpq 5085  genpnnp 5108  ltaddpr 5140  reclem3pr 5158  reclem4pr 5159  suppsrlem 5221  suppsr3 5224  suprelem 5259  elfz4t 6475  abslt 6875  absle 6876  cau2 6913  fsum1 7005  ser1clim0 7173  unctb 7577  cnsscnp 7772  nmoubi 8435  nmopubt 9832  nmfnleubt 9849  mdbr3 10224  mdbr4 10225  atssmat 10305  atcvatlem 10312  uninqs 10441  hmphre 10530  iintlem1 10632  mrdmcd 10722

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