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

Theorem biimprcd 240
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 237 1 (𝜒 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  biimparc  503  ax12i  1936  moanim  2558  euan  2559  eleq1a  2725  ceqsalgALT  3262  cgsexg  3269  cgsex2g  3270  cgsex4g  3271  ceqsex  3272  spc2egv  3326  spc3egv  3328  reu6  3428  csbiebt  3586  dfiin2g  4585  reusv2lem2  4899  ralxfrALT  4917  opelxp  5180  ssrel  5241  ssrelOLD  5242  ssrel2  5244  ssrelrel  5254  iss  5482  ordun  5867  riotaclb  6689  iunpw  7020  limom  7122  funcnvuni  7161  fun11iun  7168  soxp  7335  tfrlem8  7525  oaordex  7683  eroveu  7885  fundmen  8071  nneneq  8184  onfin2  8193  dif1en  8234  unfilem1  8265  rankwflemb  8694  sornom  9137  isf32lem9  9221  axdc3lem2  9311  axdc4lem  9315  zorn2lem3  9358  zorn2lem7  9362  tskuni  9643  grur1a  9679  grothomex  9689  genpnnp  9865  ltaddpr  9894  reclem4pr  9910  supadd  11029  supmullem1  11031  uzin  11758  elfzmlbp  12489  isfinite4  13191  brfi1uzind  13318  swrdnd  13478  sqrlem6  14032  sqreulem  14143  fvprmselgcd1  15796  lubun  17170  lspsneq  19170  fvmptnn04ifb  20704  fbasfip  21719  alexsubALTlem2  21899  ovolunlem1  23311  dchrisum0flb  25244  brbtwn2  25830  axcontlem8  25896  isclwwlknx  26998  clwwlknwwlksnb  27019  mdbr3  29284  mdbr4  29285  atssma  29365  atcvatlem  29372  ssrelf  29553  nepss  31725  sotr3  31782  fprb  31795  nodmon  31928  noextendseq  31945  nocvxminlem  32018  hfun  32410  bj-ax12ig  32740  finxpreclem2  33357  indexdom  33659  fdc  33671  totbndss  33706  grpomndo  33804  iss2  34252  ax12eq  34545  ax12el  34546  lsatn0  34604  lsatcmp  34608  lsatcv0  34636  lfl1dim  34726  lfl1dim2N  34727  lkrss2N  34774  lub0N  34794  glb0N  34798  ispsubcl2N  35551  cdlemefrs29bpre0  36001  dihglblem2N  36900  dihglblem3N  36901  dochsnnz  37056  pm13.14  38927  tratrb  39063  ax6e2ndeq  39092  3impexpbicomVD  39406  tratrbVD  39411  equncomVD  39418  trsbcVD  39427  sbcssgVD  39433  csbingVD  39434  onfrALTVD  39441  csbsngVD  39443  csbxpgVD  39444  csbresgVD  39445  csbrngVD  39446  csbima12gALTVD  39447  csbunigVD  39448  csbfv12gALTVD  39449  con5VD  39450  hbimpgVD  39454  hbexgVD  39456  ax6e2ndeqVD  39459  supxrleubrnmpt  39945  suprleubrnmpt  39962  infxrgelbrnmpt  39996  isassintop  42171  zgtp1leeq  42636
  Copyright terms: Public domain W3C validator