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

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

Proof of Theorem biimpac
StepHypRef Expression
1 biimpa.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimpcd 217 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 420 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  gencbvex2  3008  2reu5  3151  ordnbtwn  4707  onsucuni2  4849  poltletr  5304  tz6.12-1  5778  nfunsn  5792  smo11  6662  omlimcl  6857  th3qlem1  7046  omxpenlem  7245  fodomr  7294  fodomfib  7422  r1val1  7748  alephval3  8029  dfac5lem4  8045  dfac5  8047  axdc4lem  8373  fodomb  8442  distrlem1pr  8940  map2psrpr  9023  supsrlem  9024  eqle  9214  sumz  12554  divalglem8  12958  pospo  14468  lsmcv  16251  opsrtoslem1  16582  psrbagsuppfi  16603  hauscmplem  17507  ptbasfi  17651  hmphindis  17867  fbncp  17909  fgcl  17948  fixufil  17992  uffixfr  17993  mbfima  19560  mbfimaicc  19561  ig1pdvds  20137  uhgraun  21384  eupai  21727  spansncvi  23192  eigposi  23377  pjnormssi  23709  sumdmdlem  23959  rhmdvdsr  24291  rtrclind  25184  prod1  25305  ax5seglem4  25906  axcontlem2  25939  axcontlem4  25941  cgrdegen  25973  btwnconn1lem11  26066  btwnconn1lem12  26067  btwnconn1lem14  26069  isbnd2  26534  pm13.13a  27696  iotavalb  27719  2cshwcom  28399  usgfiregdegfi  28524  usgreghash2spot  28630  biimpa21  28828  suctrALTcf  29208  suctrALTcfVD  29209  suctrALT3  29210  unisnALT  29212  bnj168  29271  bnj521  29278  bnj964  29488  bnj966  29489  bnj1398  29577  atcvrj0  30399  paddasslem5  30795
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 179  df-an 362
  Copyright terms: Public domain W3C validator