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

Theorem biimp3ar 1330
Description: Infer implication from a logical equivalence. Similar to biimpar 485. (Contributed by NM, 2-Jan-2009.)
Hypothesis
Ref Expression
biimp3a.1  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
Assertion
Ref Expression
biimp3ar  |-  ( (
ph  /\  ps  /\  th )  ->  ch )

Proof of Theorem biimp3ar
StepHypRef Expression
1 biimp3a.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
21exbiri 622 . 2  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
323imp 1191 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 974
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  df-3an 976
This theorem is referenced by:  rmoi  3417  brelrng  5222  div2sub  10375  ssfzo12  11884  modltm1p1mod  12018  abssubge0  13139  qredeu  14125  abvne0  17350  slesolinvbi  19056  basgen2  19364  fcfval  20407  nmne0  21011  ovolfsf  21756  lgssq  23482  lgssq2  23483  colinearalg  24085  nv1  25451  adjeq  26726  areacirc  30087  fvopabf4g  30186  exidreslem  30314  iocmbl  31156  ssfz12  32168  iunconlem2  33468  hgmapvvlem3  37395
  Copyright terms: Public domain W3C validator