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

Theorem biimparc 485
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 225 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
32imp 427 1  |-  ( ( ch  /\  ph )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
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  df-an 369
This theorem is referenced by:  biantr  929  elrab3t  3194  difprsnss  4092  elpw2g  4541  elon2  4816  ideqg  5080  elrnmpt1s  5176  elrnmptg  5178  eqfnfv2  5897  fmpt  5967  elunirn  6080  fun11iun  6677  tposfo2  6914  tposf12  6916  dom2lem  7492  enfii  7671  ssnnfi  7673  ac6sfi  7697  unfilem1  7717  inf3lem2  7978  infdiffi  8006  dfac5lem5  8439  dfac2  8442  dfac12k  8458  cfslb2n  8579  enfin2i  8632  fin23lem19  8647  axdc2lem  8759  axdc3lem4  8764  winainflem  9000  indpi  9214  ltexnq  9282  ltbtwnnq  9285  ltexprlem6  9348  prlem936  9354  elreal2  9438  fimaxre3  10426  expnbnd  12216  repswswrd  12686  climcnds  13684  fprod2dlem  13805  unbenlem  14447  acsfn  15085  lsmcv  17919  maducoeval2  19246  bastop2  19600  neipeltop  19735  rnelfmlem  20557  isfcls  20614  tgphaus  20719  mbfi1fseqlem4  22229  ulm2  22884  ax5seglem5  24378  wlkdvspthlem  24751  wlknwwlknsur  24854  spanunsni  26635  nonbooli  26707  nmopun  27070  lncnopbd  27093  pjnmopi  27204  sumdmdlem  27474  spc2ed  27510  disjun0  27614  rnmpt2ss  27691  esumpcvgval  28257  soseq  29535  btwnconn1lem7  29932  ovoliunnfl  30257  voliunnfl  30259  volsupnfl  30260  ivthALT  30355  topfneec  30375  fdc  30440  ismtyres  30506  isdrngo3  30564  isnumbasgrplem3  31258  pm13.13b  31519  fprodle  31805  nn0sumshdiglemB  33476  ax6e2ndeqALT  34113  sineq0ALT  34119  bnj545  34335  bnj900  34369  bnj1498  34499  bj-snglss  34911  lshpset2N  35292  3dimlem1  35630  3dim3  35641  cdleme31fv2  36567
  Copyright terms: Public domain W3C validator