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

Theorem 3anbi3d 1254
Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
Hypothesis
Ref Expression
3anbi1d.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
3anbi3d  |-  ( ph  ->  ( ( th  /\  ta  /\  ps )  <->  ( th  /\  ta  /\  ch )
) )

Proof of Theorem 3anbi3d
StepHypRef Expression
1 biidd 170 . 2  |-  ( ph  ->  ( th  <->  th )
)
2 3anbi1d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 23anbi13d 1250 1  |-  ( ph  ->  ( ( th  /\  ta  /\  ps )  <->  ( th  /\  ta  /\  ch )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> 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:  ceqsex3v  2661  ceqsex4v  2662  ceqsex8v  2664  vtocl3gaf  2688  mob  2797  ordsoexmid  4378  tfr1onlemaccex  6113  tfrcllemaccex  6126  fseq1m1p1  9509  isummo  10773  fisum  10778  divalglemnn  11196  divalglemeunn  11199  divalglemex  11200  divalglemeuneg  11201
  Copyright terms: Public domain W3C validator