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

Theorem biimpcd 215
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 19 . 2  |-  ( ps 
->  ps )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibcom 211 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  biimpac  472  3impexpbicom  1357  ax16i  1986  ax16ALT2  1988  nfsb4t  2020  nelneq  2381  nelneq2  2382  nelne1  2535  nelne2  2536  nssne1  3234  nssne2  3235  psssstr  3282  difsn  3755  iununi  3986  disjiun  4013  nbrne1  4040  nbrne2  4041  mosubopt  4264  tz7.7  4418  limsssuc  4641  nnsuc  4673  peano5  4679  issref  5056  tz6.12i  5548  ssimaex  5584  chfnrn  5636  ffnfv  5685  f1elima  5787  dftpos4  6253  odi  6577  fineqvlem  7077  pssnn  7081  ordunifi  7107  wdom2d  7294  r1pwss  7456  alephval3  7737  infdif  7835  cff1  7884  cofsmo  7895  axdc3lem2  8077  zorn2lem6  8128  cfpwsdom  8206  prub  8618  prnmadd  8621  1re  8837  letr  8914  addid1  8992  xrletr  10489  0fz1  10813  leisorel  11398  sqrmo  11737  dvdseq  12576  isprm2  12766  nprmdvds1  12790  pltletr  14105  sylow2alem2  14929  islss  15692  gzrngunitlem  16436  pjdm2  16611  isclo2  16825  fbasfip  17563  ufileu  17614  alexsubALTlem2  17742  ismgm  20987  5oalem6  22238  eigorthi  22417  adjbd1o  22665  dmdbr7ati  23004  ceqsrexv2  24078  dedekindle  24083  dfpo2  24112  fundmpss  24122  funbreq  24127  idinside  24707  wl-pm5.74lem  24917  prj1b  25079  prj3  25080  eloi  25086  cur1vald  25199  cmptdst  25568  limptlimpr2lem1  25574  addcanrg  25667  iscol3  26094  sdclem2  26452  fdc1  26456  rfcnnnub  27707  funressnfv  27991  ffnafv  28033  sbcim2g  28302  suctrALT2VD  28612  suctrALT2  28613  3impexpVD  28632  3impexpbicomVD  28633  sbcim2gVD  28651  csbeq2gVD  28668  csbsngVD  28669  a9e2ndeqVD  28685  2sb5ndVD  28686  a12study4  29117  lsatcvatlem  29239  atnle  29507  cvratlem  29610  ispsubcl2N  30136  trlord  30758  diaelrnN  31235  cdlemm10N  31308  dochexmidlem7  31656
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 177
  Copyright terms: Public domain W3C validator