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

Theorem biimparc 487
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 429 1  |-  ( ( ch  /\  ph )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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 371
This theorem is referenced by:  biantr  922  elrab3t  3116  difprsnss  4009  elpw2g  4455  elon2  4730  ideqg  4991  elrnmpt1s  5087  elrnmptg  5089  eqfnfv2  5798  fmpt  5864  elunirn  5968  fun11iun  6537  tposfo2  6768  tposf12  6770  dom2lem  7349  enfii  7530  ssnnfi  7532  ac6sfi  7556  unfilem1  7576  inf3lem2  7835  infdiffi  7863  dfac5lem5  8297  dfac2  8300  dfac12k  8316  cfslb2n  8437  enfin2i  8490  fin23lem19  8505  axdc2lem  8617  axdc3lem4  8622  winainflem  8860  gruiun  8966  indpi  9076  ltexnq  9144  ltbtwnnq  9147  ltexprlem6  9210  prlem936  9216  elreal2  9299  fimaxre3  10279  expnbnd  11993  repswswrd  12422  climcnds  13314  unbenlem  13969  acsfn  14597  lsmcv  17222  maducoeval2  18446  bastop2  18599  neipeltop  18733  rnelfmlem  19525  isfcls  19582  tgphaus  19687  mbfi1fseqlem4  21196  ulm2  21850  ax5seglem5  23179  wlkdvspthlem  23506  spanunsni  24982  nonbooli  25054  nmopun  25418  lncnopbd  25441  pjnmopi  25552  sumdmdlem  25822  spc2ed  25857  rnmpt2ss  25992  esumpcvgval  26527  soseq  27715  btwnconn1lem7  28124  ovoliunnfl  28433  voliunnfl  28435  volsupnfl  28436  ivthALT  28530  topfneec  28563  fdc  28641  ismtyres  28707  isdrngo3  28765  isnumbasgrplem3  29461  pm13.13b  29662  wlknwwlknsur  30344  ax6e2ndeqALT  31667  sineq0ALT  31673  bnj545  31888  bnj900  31922  bnj1498  32052  bj-snglss  32463  lshpset2N  32764  3dimlem1  33102  3dim3  33113  cdleme31fv2  34037
  Copyright terms: Public domain W3C validator