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

Theorem 3anbi123d 1248
Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)
Hypotheses
Ref Expression
bi3d.1  |-  ( ph  ->  ( ps  <->  ch )
)
bi3d.2  |-  ( ph  ->  ( th  <->  ta )
)
bi3d.3  |-  ( ph  ->  ( et  <->  ze )
)
Assertion
Ref Expression
3anbi123d  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  <->  ( ch  /\ 
ta  /\  ze )
) )

Proof of Theorem 3anbi123d
StepHypRef Expression
1 bi3d.1 . . . 4  |-  ( ph  ->  ( ps  <->  ch )
)
2 bi3d.2 . . . 4  |-  ( ph  ->  ( th  <->  ta )
)
31, 2anbi12d 457 . . 3  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  ta ) ) )
4 bi3d.3 . . 3  |-  ( ph  ->  ( et  <->  ze )
)
53, 4anbi12d 457 . 2  |-  ( ph  ->  ( ( ( ps 
/\  th )  /\  et ) 
<->  ( ( ch  /\  ta )  /\  ze )
) )
6 df-3an 926 . 2  |-  ( ( ps  /\  th  /\  et )  <->  ( ( ps 
/\  th )  /\  et ) )
7 df-3an 926 . 2  |-  ( ( ch  /\  ta  /\  ze )  <->  ( ( ch 
/\  ta )  /\  ze ) )
85, 6, 73bitr4g 221 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  <->  ( ch  /\ 
ta  /\  ze )
) )
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:  3anbi12d  1249  3anbi13d  1250  3anbi23d  1251  limeq  4195  smoeq  6037  tfrlemi1  6079  tfr1onlemaccex  6095  tfrcllemaccex  6108  ereq1  6279  updjud  6752  elinp  7012  iccshftr  9380  iccshftl  9382  iccdil  9384  icccntr  9386  fzaddel  9441  elfzomelpfzo  9607  seq3f1olemstep  9895  seq3f1olemp  9896  sumeq1  10708  isummolem2  10736  isummo  10737  zisum  10738  divalglemnn  11011  divalglemeunn  11014  divalglemeuneg  11016  dfgcd2  11096
  Copyright terms: Public domain W3C validator