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

Theorem 3anbi123d 1273
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 462 . . 3  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  ta ) ) )
4 bi3d.3 . . 3  |-  ( ph  ->  ( et  <->  ze )
)
53, 4anbi12d 462 . 2  |-  ( ph  ->  ( ( ( ps 
/\  th )  /\  et ) 
<->  ( ( ch  /\  ta )  /\  ze )
) )
6 df-3an 947 . 2  |-  ( ( ps  /\  th  /\  et )  <->  ( ( ps 
/\  th )  /\  et ) )
7 df-3an 947 . 2  |-  ( ( ch  /\  ta  /\  ze )  <->  ( ( ch 
/\  ta )  /\  ze ) )
85, 6, 73bitr4g 222 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  <->  ( ch  /\ 
ta  /\  ze )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    /\ w3a 945
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 947
This theorem is referenced by:  3anbi12d  1274  3anbi13d  1275  3anbi23d  1276  limeq  4267  smoeq  6153  tfrlemi1  6195  tfr1onlemaccex  6211  tfrcllemaccex  6224  ereq1  6402  updjud  6933  ctssdclemr  6963  elinp  7246  sup3exmid  8675  iccshftr  9728  iccshftl  9730  iccdil  9732  icccntr  9734  fzaddel  9790  elfzomelpfzo  9959  seq3f1olemstep  10225  seq3f1olemp  10226  sumeq1  11075  summodclem2  11102  summodc  11103  zsumdc  11104  divalglemnn  11522  divalglemeunn  11525  divalglemeuneg  11527  dfgcd2  11609  ctiunct  11859  isstruct2im  11875  isstruct2r  11876  fiinopn  12077  lmfval  12267  upxp  12347
  Copyright terms: Public domain W3C validator