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

Theorem biimpac 473
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 216 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 419 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  gencbvex2  2999  2reu5  3142  ordnbtwn  4672  onsucuni2  4814  poltletr  5269  tz6.12-1  5747  nfunsn  5761  smo11  6626  omlimcl  6821  th3qlem1  7010  omxpenlem  7209  fodomr  7258  fodomfib  7386  r1val1  7712  alephval3  7991  dfac5lem4  8007  dfac5  8009  axdc4lem  8335  fodomb  8404  distrlem1pr  8902  map2psrpr  8985  supsrlem  8986  eqle  9176  sumz  12516  divalglem8  12920  pospo  14430  lsmcv  16213  opsrtoslem1  16544  psrbagsuppfi  16565  hauscmplem  17469  ptbasfi  17613  hmphindis  17829  fbncp  17871  fgcl  17910  fixufil  17954  uffixfr  17955  mbfima  19524  mbfimaicc  19525  ig1pdvds  20099  uhgraun  21346  eupai  21689  spansncvi  23154  eigposi  23339  pjnormssi  23671  sumdmdlem  23921  rhmdvdsr  24256  rtrclind  25149  prod1  25270  ax5seglem4  25871  axcontlem2  25904  axcontlem4  25906  cgrdegen  25938  btwnconn1lem11  26031  btwnconn1lem12  26032  btwnconn1lem14  26034  isbnd2  26492  pm13.13a  27584  iotavalb  27607  2cshwcom  28267  usgfiregdegfi  28361  usgreghash2spot  28458  biimpa21  28656  suctrALTcf  29034  suctrALTcfVD  29035  suctrALT3  29036  unisnALT  29038  bnj168  29097  bnj521  29104  bnj964  29314  bnj966  29315  bnj1398  29403  atcvrj0  30225  paddasslem5  30621
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