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

Theorem biimparc 474
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 217 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
32imp 419 1  |-  ( ( ch  /\  ph )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  biantr  898  difprsnss  3926  elpw2g  4355  elon2  4584  ideqg  5016  elrnmpt1s  5110  elrnmptg  5112  fun11iun  5687  eqfnfv2  5820  fmpt  5882  elunirnALT  5992  tposfo2  6494  tposf12  6496  dom2lem  7139  enfii  7318  ssnnfi  7320  ac6sfi  7343  unfilem1  7363  inf3lem2  7576  infdiffi  7604  dfac5lem5  8000  dfac2  8003  dfac12k  8019  cfslb2n  8140  enfin2i  8193  fin23lem19  8208  axdc2lem  8320  axdc3lem4  8325  winainflem  8560  gruiun  8666  indpi  8776  ltexnq  8844  ltbtwnnq  8847  ltexprlem6  8910  prlem936  8916  elreal2  8999  fimaxre3  9949  expnbnd  11500  climcnds  12623  unbenlem  13268  acsfn  13876  lsmcv  16205  bastop2  17051  neipeltop  17185  rnelfmlem  17976  isfcls  18033  tgphaus  18138  mbfi1fseqlem4  19602  ulm2  20293  wlkdvspthlem  21599  spanunsni  23073  nonbooli  23145  nmopun  23509  lncnopbd  23532  pjnmopi  23643  sumdmdlem  23913  rnmpt2ss  24078  esumpcvgval  24460  soseq  25521  ax5seglem5  25864  btwnconn1lem7  26019  ovoliunnfl  26238  voliunnfl  26240  volsupnfl  26241  ivthALT  26329  topfneec  26362  fdc  26440  ismtyres  26508  isdrngo3  26566  isnumbasgrplem3  27238  pm13.13b  27576  a9e2ndeqALT  28980  sineq0ALT  28986  bnj545  29203  bnj900  29237  bnj1498  29367  lshpset2N  29854  3dimlem1  30192  3dim3  30203  cdleme31fv2  31127
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  df-an 361
  Copyright terms: Public domain W3C validator