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

Theorem biimparc 494
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimparc  |-  ( ( ch  /\  ph )  ->  ps )

Proof of Theorem biimparc
StepHypRef Expression
1 biimpa.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimprcd 233 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
32imp 435 1  |-  ( ( ch  /\  ph )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  biantr  942  elrab3t  3163  difprsnss  4076  elpw2g  4539  ideqg  4964  elrnmpt1s  5060  elrnmptg  5062  elon2  5413  eqfnfv2  5961  fmpt  6027  elunirn  6142  fun11iun  6741  tposfo2  6983  tposf12  6985  dom2lem  7596  enfii  7776  ssnnfi  7778  ac6sfi  7802  unfilem1  7822  inf3lem2  8121  infdiffi  8150  dfac5lem5  8545  dfac2  8548  dfac12k  8564  cfslb2n  8685  enfin2i  8738  fin23lem19  8753  axdc2lem  8865  axdc3lem4  8870  winainflem  9105  indpi  9319  ltexnq  9387  ltbtwnnq  9390  ltexprlem6  9453  prlem936  9459  elreal2  9543  fimaxre3  10542  expnbnd  12395  opfi1uzind  12649  repswswrd  12886  climcnds  13920  fprod2dlem  14045  fprodle  14061  unbenlem  14863  acsfn  15576  lsmcv  18375  maducoeval2  19676  bastop2  20021  neipeltop  20156  rnelfmlem  20978  isfcls  21035  tgphaus  21142  mbfi1fseqlem4  22688  ulm2  23352  ax5seglem5  24975  wlkdvspthlem  25349  wlknwwlknsur  25452  spanunsni  27244  nonbooli  27316  nmopun  27679  lncnopbd  27702  pjnmopi  27813  sumdmdlem  28083  spc2ed  28118  disjun0  28215  rnmpt2ss  28284  esumpcvgval  28906  bnj545  29712  bnj900  29746  bnj1498  29876  soseq  30498  btwnconn1lem7  30866  ivthALT  30997  topfneec  31017  bj-snglss  31566  mptsnunlem  31742  icoreresf  31757  poimirlem14  31956  poimirlem22  31964  poimirlem26  31968  poimirlem29  31971  ovoliunnfl  31984  voliunnfl  31986  volsupnfl  31987  fdc  32076  ismtyres  32142  isdrngo3  32200  lshpset2N  32687  3dimlem1  33025  3dim3  33036  cdleme31fv2  33962  isnumbasgrplem3  35966  pm13.13b  36760  ax6e2ndeqALT  37325  sineq0ALT  37331  elrnmpt1sf  37474  1wlkdlem4  39780  31wlkdlem4  39955  nn0sumshdiglemB  40756
  Copyright terms: Public domain W3C validator