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

Theorem biimprcd 253
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 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
biimprcd (𝜒 → (𝜑𝜓))

Proof of Theorem biimprcd
StepHypRef Expression
1 id 22 . 2 (𝜒𝜒)
2 biimpcd.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5ibrcom 250 1 (𝜒 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  biimparc  483  ax12i  1969  moanimlem  2683  euan  2686  euanv  2689  eleq1a  2888  ceqsalgALT  3480  cgsexg  3487  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  ceqsex  3491  spcegv  3548  spc2egv  3551  reu6  3668  csbiebt  3860  dfiin2g  4922  reusv2lem2  5268  ralxfrALT  5284  opelxp  5559  ssrel  5625  ssrel2  5627  ssrelrel  5637  iss  5874  ordun  6264  fprb  6937  riotaclb  7138  iunpw  7477  limom  7579  funcnvuni  7622  fiunlem  7629  soxp  7810  tfrlem8  8007  oaordex  8171  eroveu  8379  fundmen  8570  nneneq  8688  onfin2  8699  dif1en  8739  unfilem1  8770  rankwflemb  9210  sornom  9692  isf32lem9  9776  axdc3lem2  9866  axdc4lem  9870  zorn2lem3  9913  zorn2lem7  9917  tskuni  10198  grur1a  10234  grothomex  10244  genpnnp  10420  ltaddpr  10449  reclem4pr  10465  supadd  11600  supmullem1  11602  uzin  12270  elfzmlbp  13017  isfinite4  13723  brfi1uzind  13856  swrdnd  14011  sqrlem6  14602  sqreulem  14714  fvprmselgcd1  16374  lubun  17728  lspsneq  19890  fvmptnn04ifb  21459  fbasfip  22476  alexsubALTlem2  22656  ovolunlem1  24104  dchrisum0flb  26097  brbtwn2  26702  axcontlem8  26768  isclwwlknx  27824  clwwlkel  27834  clwwlknwwlksnb  27843  wwlksext2clwwlk  27845  mdbr3  30083  mdbr4  30084  atssma  30164  atcvatlem  30171  ssrelf  30382  nepss  33056  sotr3  33110  nodmon  33265  noextendseq  33282  nocvxminlem  33355  hfun  33747  bj-ax12ig  34077  bj-substw  34164  finxpreclem2  34802  indexdom  35165  fdc  35176  totbndss  35208  grpomndo  35306  iss2  35754  ax12eq  36230  ax12el  36231  lsatn0  36288  lsatcmp  36292  lsatcv0  36320  lfl1dim  36410  lfl1dim2N  36411  lkrss2N  36458  lub0N  36478  glb0N  36482  ispsubcl2N  37236  cdlemefrs29bpre0  37685  dihglblem2N  38583  dihglblem3N  38584  dochsnnz  38739  pm13.14  41100  tratrb  41229  ax6e2ndeq  41252  3impexpbicomVD  41550  tratrbVD  41554  equncomVD  41561  trsbcVD  41570  sbcssgVD  41576  csbingVD  41577  onfrALTVD  41584  csbsngVD  41586  csbxpgVD  41587  csbresgVD  41588  csbrngVD  41589  csbima12gALTVD  41590  csbunigVD  41591  csbfv12gALTVD  41592  con5VD  41593  hbimpgVD  41597  hbexgVD  41599  ax6e2ndeqVD  41602  supxrleubrnmpt  42030  suprleubrnmpt  42046  infxrgelbrnmpt  42080  isassintop  44457  zgtp1leeq  44917
  Copyright terms: Public domain W3C validator