MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimprcd Structured version   Unicode version

Theorem biimprcd 225
Description: Deduce a converse commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
Hypothesis
Ref Expression
biimpcd.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimprcd  |-  ( ch 
->  ( ph  ->  ps ) )

Proof of Theorem biimprcd
StepHypRef Expression
1 id 22 . 2  |-  ( ch 
->  ch )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibrcom 222 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  biimparc  484  ax12i  1698  axc9lem1  1944  axc9lem2  1987  ax12eq  2243  ax12el  2244  moanim  2327  euan  2328  eleq1a  2502  ceqsalg  2987  cgsexg  2994  cgsex2g  2995  cgsex4g  2996  ceqsex  2997  spc2egv  3048  spc3egv  3050  csbiebt  3296  dfiin2g  4191  ralxfrALT  4499  ordun  4807  opelxp  4856  ssrel  4915  ssrel2  4917  ssrelrel  4927  iss  5142  riotaclb  6079  iunpw  6379  limom  6480  funcnvuni  6519  fun11iun  6526  soxp  6674  tfrlem8  6829  abianfp  6900  oaordex  6985  eroveu  7183  fundmen  7371  nneneq  7482  onfin2  7490  dif1enOLD  7532  dif1en  7533  unfilem1  7564  rankwflemb  7988  sornom  8434  isf32lem9  8518  axdc3lem2  8608  axdc4lem  8612  zorn2lem3  8655  zorn2lem7  8659  tskuni  8937  grur1a  8973  grothomex  8983  genpnnp  9161  ltaddpr  9190  reclem4pr  9206  supmullem1  10283  uzin  10880  elfzmlbp  11477  sqrlem6  12720  sqreulem  12830  isprm2lem  13752  lubun  15275  lspsneq  17124  fbasfip  19282  alexsubALTlem2  19461  ovolunlem1  20821  dchrisum0flb  22643  brbtwn2  22973  axcontlem8  23039  usgranloopv  23119  grpomndo  23655  mdbr3  25523  mdbr4  25524  atssma  25604  atcvatlem  25611  ssrelf  25768  nepss  27220  fprb  27430  frrlem4  27617  nodmon  27637  nodenselem4  27671  nocvxminlem  27677  nofulllem4  27692  nofulllem5  27693  hfun  28062  supadd  28259  indexdom  28469  fdc  28482  totbndss  28517  ceqsex3OLD  28847  pm13.14  29505  rusgrargra  30390  frgrancvvdeqlemC  30475  tratrb  30940  ax6e2ndeq  30966  3impexpbicomVD  31292  tratrbVD  31296  equncomVD  31303  trsbcVD  31312  sbcssgVD  31318  csbingVD  31319  onfrALTVD  31326  csbsngVD  31328  csbxpgVD  31329  csbresgVD  31330  csbrngVD  31331  csbima12gALTVD  31332  csbunigVD  31333  csbfv12gALTVD  31334  con5VD  31335  hbimpgVD  31339  hbexgVD  31341  ax6e2ndeqVD  31344  bj-ax12i  31824  lsatn0  32214  lsatcmp  32218  lsatcv0  32246  lfl1dim  32336  lfl1dim2N  32337  lkrss2N  32384  lub0N  32404  glb0N  32408  ispsubcl2N  33161  cdlemefrs29bpre0  33610  dihglblem2N  34509  dihglblem3N  34510  dochsnnz  34665
  Copyright terms: Public domain W3C validator