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

Theorem biimpcd 224
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 22 . 2  |-  ( ps 
->  ps )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibcom 220 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  biimpac  486  axc16i  2012  nelneq  2544  nelneq2  2545  nelne1  2722  nelne2  2723  nssne1  3433  nssne2  3434  psssstr  3483  difsn  4029  iununi  4276  disjiun  4303  nbrne1  4330  nbrne2  4331  mosubopt  4610  tz7.7  4766  issref  5232  tz6.12i  5731  ssimaex  5777  chfnrn  5835  ffnfv  5890  f1elima  5997  limsssuc  6482  nnsuc  6514  peano5  6520  dftpos4  6785  odi  7039  fineqvlem  7548  pssnn  7552  ordunifi  7583  wdom2d  7816  r1pwss  8012  alephval3  8301  infdif  8399  cff1  8448  cofsmo  8459  axdc3lem2  8641  zorn2lem6  8691  cfpwsdom  8769  prub  9184  prnmadd  9187  1re  9406  letr  9489  dedekindle  9555  addid1  9570  xrletr  11153  0fz1  11490  elfzmlbp  11512  leisorel  12234  brfi1uzind  12240  swrdccatfn  12394  sqrmo  12762  dvdseq  13601  isprm2  13792  nprmdvds1  13818  pltletr  15162  fvcosymgeq  15955  sylow2alem2  16138  islss  17038  gsumply1subr  17710  gzrngunitlem  17899  pjdm2  18158  isclo2  18714  fbasfip  19463  ufileu  19514  alexsubALTlem2  19642  cnextcn  19661  metustblOLD  20177  metustbl  20178  usgrarnedg1  23329  nbgraf1olem3  23374  nbgraf1olem5  23376  nb3graprlem1  23381  cusgrafilem2  23410  fargshiftfo  23546  3v3e3cycl1  23552  4cycl4v4e  23574  4cycl4dv4e  23576  ismgm  23829  5oalem6  25084  eigorthi  25263  adjbd1o  25511  dmdbr7ati  25850  dfpo2  27587  fundmpss  27599  funbreq  27604  idinside  28137  sdclem2  28664  fdc1  28668  funressnfv  30060  ffnafv  30103  elovmpt3rab1  30189  exprelprel  30255  wlkn0  30305  wlkiswwlk2lem3  30353  wlklniswwlkn1  30359  wlklniswwlkn2  30360  wwlknext  30382  el2wlkonot  30414  el2wlkonotot1  30419  clwwlknimp  30465  clwlkisclwwlklem2a1  30467  clwlkisclwwlklem2a  30473  clwwlkel  30481  clwwlkext2edg  30490  wwlkext2clwwlk  30491  clwwisshclwwlem  30496  hashecclwwlkn1  30534  usghashecclwwlk  30535  clwlkfclwwlk  30543  clwlkf1clwwlklem2  30546  frgrancvvdeqlemA  30656  frgrancvvdeqlemC  30658  frgraeu  30673  numclwlk2lem2f  30722  numclwlk2lem2f1o  30724  frgraogt3nreg  30739  assamulgscmlem2  30854  dmatmul  30915  mat2pmatlin  31086  pmatcollpw1dstlem1  31115  3impexpbicom  31252  sbcim2g  31341  suctrALT2VD  31668  suctrALT2  31669  3impexpVD  31688  3impexpbicomVD  31689  sbcim2gVD  31707  csbeq2gVD  31724  csbsngVD  31725  ax6e2ndeqVD  31741  2sb5ndVD  31742  lsatcvatlem  32790  atnle  33058  cvratlem  33161  ispsubcl2N  33687  trlord  34309  diaelrnN  34786  cdlemm10N  34859  dochexmidlem7  35207
  Copyright terms: Public domain W3C validator