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

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

Proof of Theorem biimpcd
StepHypRef Expression
1 id 21 . 2  |-  ( ps 
->  ps )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibcom 213 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  biimpac  474  3impexpbicom  1377  ax16i  2055  nfsb4tOLD  2133  ax16ALT2  2162  nelneq  2541  nelneq2  2542  nelne1  2700  nelne2  2701  nssne1  3393  nssne2  3394  psssstr  3442  difsn  3962  iununi  4206  disjiun  4233  nbrne1  4260  nbrne2  4261  mosubopt  4489  tz7.7  4642  limsssuc  4865  nnsuc  4897  peano5  4903  issref  5282  tz6.12i  5782  ssimaex  5824  chfnrn  5877  ffnfv  5930  f1elima  6045  dftpos4  6534  odi  6858  fineqvlem  7359  pssnn  7363  ordunifi  7393  wdom2d  7584  r1pwss  7746  alephval3  8029  infdif  8127  cff1  8176  cofsmo  8187  axdc3lem2  8369  zorn2lem6  8419  cfpwsdom  8497  prub  8909  prnmadd  8912  1re  9128  letr  9205  addid1  9284  xrletr  10786  0fz1  11112  leisorel  11747  brfi1uzind  11753  sqrmo  12095  dvdseq  12935  isprm2  13125  nprmdvds1  13149  pltletr  14466  sylow2alem2  15290  islss  16049  gzrngunitlem  16801  pjdm2  16976  isclo2  17190  fbasfip  17938  ufileu  17989  alexsubALTlem2  18117  cnextcn  18136  metustblOLD  18648  metustbl  18649  usgrarnedg1  21446  nbgraf1olem3  21491  nbgraf1olem5  21493  nb3graprlem1  21498  cusgrafilem2  21527  fargshiftfo  21663  3v3e3cycl1  21669  4cycl4v4e  21691  4cycl4dv4e  21693  ismgm  21946  5oalem6  23199  eigorthi  23378  adjbd1o  23626  dmdbr7ati  23965  dedekindle  25223  dfpo2  25413  fundmpss  25425  funbreq  25430  idinside  26053  wl-pm5.74lem  26262  sdclem2  26488  fdc1  26492  funressnfv  28080  ffnafv  28123  elfzmlbp  28228  ubmelfzo  28247  exprelprel  28294  swrdccatfn  28336  cshweqdif2  28402  cshweqdif2s  28403  wlkn0  28430  wlkiswwlk2lem3  28473  wlklniswwlkn1  28479  wlklniswwlkn2  28480  el2wlkonot  28499  el2wlkonotot1  28504  frgrancvvdeqlemA  28598  frgrancvvdeqlemC  28600  frgraeu  28615  sbcim2g  28795  suctrALT2VD  29122  suctrALT2  29123  3impexpVD  29142  3impexpbicomVD  29143  sbcim2gVD  29161  csbeq2gVD  29178  csbsngVD  29179  a9e2ndeqVD  29195  2sb5ndVD  29196  ax16iNEW7  29725  nfsb4twAUX7  29750  ax16ALT2OLD7  29917  nfsb4tOLD7  29919  nfsb4tw2AUXOLD7  29920  lsatcvatlem  30021  atnle  30289  cvratlem  30392  ispsubcl2N  30918  trlord  31540  diaelrnN  32017  cdlemm10N  32090  dochexmidlem7  32438
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