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  1367  ax16i  2051  ax16ALT2  2053  nfsb4t  2085  nelneq  2456  nelneq2  2457  nelne1  2610  nelne2  2611  nssne1  3310  nssne2  3311  psssstr  3358  difsn  3831  iununi  4067  disjiun  4094  nbrne1  4121  nbrne2  4122  mosubopt  4346  tz7.7  4500  limsssuc  4723  nnsuc  4755  peano5  4761  issref  5138  tz6.12i  5631  ssimaex  5667  chfnrn  5719  ffnfv  5768  f1elima  5874  dftpos4  6340  odi  6664  fineqvlem  7165  pssnn  7169  ordunifi  7197  wdom2d  7384  r1pwss  7546  alephval3  7827  infdif  7925  cff1  7974  cofsmo  7985  axdc3lem2  8167  zorn2lem6  8218  cfpwsdom  8296  prub  8708  prnmadd  8711  1re  8927  letr  9004  addid1  9082  xrletr  10581  0fz1  10905  leisorel  11494  sqrmo  11833  dvdseq  12673  isprm2  12863  nprmdvds1  12887  pltletr  14204  sylow2alem2  15028  islss  15791  gzrngunitlem  16542  pjdm2  16717  isclo2  16931  fbasfip  17665  ufileu  17716  alexsubALTlem2  17844  ismgm  21099  5oalem6  22352  eigorthi  22531  adjbd1o  22779  dmdbr7ati  23118  cnextcn  23504  metustbl  23610  ceqsrexv2  24482  dedekindle  24489  dfpo2  24670  fundmpss  24680  funbreq  24685  idinside  25266  wl-pm5.74lem  25476  sdclem2  25776  fdc1  25780  rfcnnnub  27030  funressnfv  27316  ffnafv  27359  brfi1uzind  27497  usgrarnedg1  27562  nbgraf1olem3  27607  nbgraf1olem5  27609  nb3graprlem1  27614  cusgrafilem2  27643  fargshiftfo  27761  3v3e3cycl1  27768  4cycl4v4e  27790  4cycl4dv4e  27792  frgrancvvdeqlemA  27870  frgrancvvdeqlemC  27872  sbcim2g  28047  suctrALT2VD  28374  suctrALT2  28375  3impexpVD  28394  3impexpbicomVD  28395  sbcim2gVD  28413  csbeq2gVD  28430  csbsngVD  28431  a9e2ndeqVD  28447  2sb5ndVD  28448  ax16iNEW7  28972  nfsb4twAUX7  28997  ax16ALT2OLD7  29144  nfsb4tOLD7  29146  nfsb4tw2AUXOLD7  29147  a12study4  29186  lsatcvatlem  29308  atnle  29576  cvratlem  29679  ispsubcl2N  30205  trlord  30827  diaelrnN  31304  cdlemm10N  31377  dochexmidlem7  31725
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