ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimp3a Unicode version

Theorem biimp3a 1251
Description: Infer implication from a logical equivalence. Similar to biimpa 284. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
biimp3a.1  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
Assertion
Ref Expression
biimp3a  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem biimp3a
StepHypRef Expression
1 biimp3a.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
21biimpa 284 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
323impa 1110 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    <-> wb 102    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  nnawordex  6132  nn0addge1  8285  nn0addge2  8286  nn0sub2  8372  eluzp1p1  8594  uznn0sub  8600  iocssre  8923  icossre  8924  iccssre  8925  lincmb01cmp  8972  iccf1o  8973  fzosplitprm1  9192  subfzo0  9199  modfzo0difsn  9345  fldivndvdslt  10247
  Copyright terms: Public domain W3C validator