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

Theorem biimp3a 1281
Description: Infer implication from a logical equivalence. Similar to biimpa 290. (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 290 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
323impa 1138 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    /\ w3a 924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  nnawordex  6287  div2subap  8302  nn0addge1  8719  nn0addge2  8720  nn0sub2  8820  eluzp1p1  9044  uznn0sub  9050  iocssre  9371  icossre  9372  iccssre  9373  lincmb01cmp  9420  iccf1o  9421  fzosplitprm1  9645  subfzo0  9653  modfzo0difsn  9802  efltim  10988  fldivndvdslt  11213  hashgcdlem  11481
  Copyright terms: Public domain W3C validator