MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimpcd Structured version   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  1376  ax16i  2130  ax16ALT2  2132  nfsb4tOLD  2155  nelneq  2533  nelneq2  2534  nelne1  2687  nelne2  2688  nssne1  3396  nssne2  3397  psssstr  3445  difsn  3925  iununi  4167  disjiun  4194  nbrne1  4221  nbrne2  4222  mosubopt  4446  tz7.7  4599  limsssuc  4822  nnsuc  4854  peano5  4860  issref  5239  tz6.12i  5743  ssimaex  5780  chfnrn  5833  ffnfv  5886  f1elima  6001  dftpos4  6490  odi  6814  fineqvlem  7315  pssnn  7319  ordunifi  7349  wdom2d  7540  r1pwss  7702  alephval3  7983  infdif  8081  cff1  8130  cofsmo  8141  axdc3lem2  8323  zorn2lem6  8373  cfpwsdom  8451  prub  8863  prnmadd  8866  1re  9082  letr  9159  addid1  9238  xrletr  10740  0fz1  11066  leisorel  11701  brfi1uzind  11707  sqrmo  12049  dvdseq  12889  isprm2  13079  nprmdvds1  13103  pltletr  14420  sylow2alem2  15244  islss  16003  gzrngunitlem  16755  pjdm2  16930  isclo2  17144  fbasfip  17892  ufileu  17943  alexsubALTlem2  18071  cnextcn  18090  metustblOLD  18602  metustbl  18603  usgrarnedg1  21400  nbgraf1olem3  21445  nbgraf1olem5  21447  nb3graprlem1  21452  cusgrafilem2  21481  fargshiftfo  21617  3v3e3cycl1  21623  4cycl4v4e  21645  4cycl4dv4e  21647  ismgm  21900  5oalem6  23153  eigorthi  23332  adjbd1o  23580  dmdbr7ati  23919  dedekindle  25180  dfpo2  25370  fundmpss  25382  funbreq  25387  idinside  26010  wl-pm5.74lem  26219  sdclem2  26437  fdc1  26441  funressnfv  27959  ffnafv  28002  elfzmlbp  28091  ubmelfzo  28109  swrdccatfn  28170  cshweqdif2  28233  cshweqdif2s  28234  el2wlkonot  28289  el2wlkonotot1  28294  frgrancvvdeqlemA  28363  frgrancvvdeqlemC  28365  frgraeu  28380  sbcim2g  28560  suctrALT2VD  28885  suctrALT2  28886  3impexpVD  28905  3impexpbicomVD  28906  sbcim2gVD  28924  csbeq2gVD  28941  csbsngVD  28942  a9e2ndeqVD  28958  2sb5ndVD  28959  ax16iNEW7  29488  nfsb4twAUX7  29513  ax16ALT2OLD7  29680  nfsb4tOLD7  29682  nfsb4tw2AUXOLD7  29683  lsatcvatlem  29784  atnle  30052  cvratlem  30155  ispsubcl2N  30681  trlord  31303  diaelrnN  31780  cdlemm10N  31853  dochexmidlem7  32201
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