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

Theorem biimpcd 216
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 20 . 2  |-  ( ps 
->  ps )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibcom 212 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  biimpac  473  3impexpbicom  1373  ax16i  2095  ax16ALT2  2097  nfsb4t  2129  nelneq  2502  nelneq2  2503  nelne1  2656  nelne2  2657  nssne1  3364  nssne2  3365  psssstr  3413  difsn  3893  iununi  4135  disjiun  4162  nbrne1  4189  nbrne2  4190  mosubopt  4414  tz7.7  4567  limsssuc  4789  nnsuc  4821  peano5  4827  issref  5206  tz6.12i  5710  ssimaex  5747  chfnrn  5800  ffnfv  5853  f1elima  5968  dftpos4  6457  odi  6781  fineqvlem  7282  pssnn  7286  ordunifi  7316  wdom2d  7504  r1pwss  7666  alephval3  7947  infdif  8045  cff1  8094  cofsmo  8105  axdc3lem2  8287  zorn2lem6  8337  cfpwsdom  8415  prub  8827  prnmadd  8830  1re  9046  letr  9123  addid1  9202  xrletr  10704  0fz1  11030  leisorel  11664  brfi1uzind  11670  sqrmo  12012  dvdseq  12852  isprm2  13042  nprmdvds1  13066  pltletr  14383  sylow2alem2  15207  islss  15966  gzrngunitlem  16718  pjdm2  16893  isclo2  17107  fbasfip  17853  ufileu  17904  alexsubALTlem2  18032  cnextcn  18051  metustblOLD  18563  metustbl  18564  usgrarnedg1  21361  nbgraf1olem3  21406  nbgraf1olem5  21408  nb3graprlem1  21413  cusgrafilem2  21442  fargshiftfo  21578  3v3e3cycl1  21584  4cycl4v4e  21606  4cycl4dv4e  21608  ismgm  21861  5oalem6  23114  eigorthi  23293  adjbd1o  23541  dmdbr7ati  23880  dedekindle  25141  dfpo2  25326  fundmpss  25336  funbreq  25341  idinside  25922  wl-pm5.74lem  26131  sdclem2  26336  fdc1  26340  funressnfv  27859  ffnafv  27902  elfzmlbp  27978  ubmelfzo  27986  el2wlkonot  28066  el2wlkonotot1  28071  frgrancvvdeqlemA  28140  frgrancvvdeqlemC  28142  frgraeu  28157  sbcim2g  28334  suctrALT2VD  28657  suctrALT2  28658  3impexpVD  28677  3impexpbicomVD  28678  sbcim2gVD  28696  csbeq2gVD  28713  csbsngVD  28714  a9e2ndeqVD  28730  2sb5ndVD  28731  ax16iNEW7  29255  nfsb4twAUX7  29280  ax16ALT2OLD7  29427  nfsb4tOLD7  29429  nfsb4tw2AUXOLD7  29430  lsatcvatlem  29532  atnle  29800  cvratlem  29903  ispsubcl2N  30429  trlord  31051  diaelrnN  31528  cdlemm10N  31601  dochexmidlem7  31949
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator