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

Theorem biimprcd 218
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 21 . 2  |-  ( ch 
->  ch )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibrcom 215 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  biimparc  475  ax11i  1658  a9e  1953  ax11eq  2272  ax11el  2273  eleq1a  2507  ceqsalg  2982  cgsexg  2989  cgsex2g  2990  cgsex4g  2991  ceqsex  2992  spc2egv  3040  spc3egv  3042  csbiebt  3289  dfiin2g  4126  ordun  4686  ralxfrALT  4745  iunpw  4762  limom  4863  opelxp  4911  ssrel  4967  ssrel2  4969  ssrelrel  4979  iss  5192  funcnvuni  5521  fun11iun  5698  soxp  6462  tfrlem8  6648  abianfp  6719  oaordex  6804  eroveu  7002  fundmen  7183  nneneq  7293  onfin2  7301  dif1enOLD  7343  dif1en  7344  unfilem1  7374  rankwflemb  7722  sornom  8162  isf32lem9  8246  axdc3lem2  8336  axdc4lem  8340  zorn2lem3  8383  zorn2lem7  8387  tskuni  8663  grur1a  8699  grothomex  8709  genpnnp  8887  ltaddpr  8916  reclem4pr  8932  supmullem1  9979  uzin  10523  sqrlem6  12058  sqreulem  12168  isprm2lem  13091  lubun  14555  lspsneq  16199  fbasfip  17905  alexsubALTlem2  18084  ovolunlem1  19398  dchrisum0flb  21209  usgranloopv  21403  grpomndo  21939  mdbr3  23805  mdbr4  23806  atssma  23886  atcvatlem  23893  nepss  25180  fprb  25402  frrlem4  25590  nodmon  25610  nodenselem4  25644  nocvxminlem  25650  nofulllem4  25665  nofulllem5  25666  brbtwn2  25849  axcontlem8  25915  hfun  26124  wl-pm5.74lem  26232  supadd  26246  indexdom  26450  fdc  26463  totbndss  26500  ceqsex3OLD  26723  pm13.14  27600  elfzmlbp  28130  rusgrargra  28445  frgrancvvdeqlemC  28502  tratrb  28694  a9e2ndeq  28720  3impexpbicomVD  29043  tratrbVD  29047  equncomVD  29054  trsbcVD  29063  sbcssVD  29069  csbingVD  29070  onfrALTVD  29077  csbsngVD  29079  csbxpgVD  29080  csbresgVD  29081  csbrngVD  29082  csbima12gALTVD  29083  csbunigVD  29084  csbfv12gALTVD  29085  con5VD  29086  hbimpgVD  29090  hbexgVD  29092  a9e2ndeqVD  29095  lubunNEW  29845  lsatn0  29871  lsatcmp  29875  lsatcv0  29903  lfl1dim  29993  lfl1dim2N  29994  lkrss2N  30041  lub0N  30061  ispsubcl2N  30818  cdlemefrs29bpre0  31267  dihglblem2N  32166  dihglblem3N  32167  dochsnnz  32322
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 179
  Copyright terms: Public domain W3C validator