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

Theorem biimp3a 1323
Description: Infer implication from a logical equivalence. Similar to biimpa 294. (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 294 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
323impa 1176 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    /\ w3a 962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  nnawordex  6417  div2subap  8589  nn0addge1  9016  nn0addge2  9017  nn0sub2  9117  eluzp1p1  9344  uznn0sub  9350  iocssre  9729  icossre  9730  iccssre  9731  lincmb01cmp  9779  iccf1o  9780  fzosplitprm1  10004  subfzo0  10012  modfzo0difsn  10161  efltim  11393  fldivndvdslt  11621  hashgcdlem  11892  tgtop11  12234  sinq12gt0  12900
  Copyright terms: Public domain W3C validator