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

Theorem 3anbi123d 1312
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 473 . . 3  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  ta ) ) )
4 bi3d.3 . . 3  |-  ( ph  ->  ( et  <->  ze )
)
53, 4anbi12d 473 . 2  |-  ( ph  ->  ( ( ( ps 
/\  th )  /\  et ) 
<->  ( ( ch  /\  ta )  /\  ze )
) )
6 df-3an 980 . 2  |-  ( ( ps  /\  th  /\  et )  <->  ( ( ps 
/\  th )  /\  et ) )
7 df-3an 980 . 2  |-  ( ( ch  /\  ta  /\  ze )  <->  ( ( ch 
/\  ta )  /\  ze ) )
85, 6, 73bitr4g 223 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  <->  ( ch  /\ 
ta  /\  ze )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    /\ w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  3anbi12d  1313  3anbi13d  1314  3anbi23d  1315  limeq  4377  smoeq  6290  tfrlemi1  6332  tfr1onlemaccex  6348  tfrcllemaccex  6361  ereq1  6541  updjud  7080  ctssdclemr  7110  tapeq1  7250  tapeq2  7251  elinp  7472  sup3exmid  8912  iccshftr  9992  iccshftl  9994  iccdil  9996  icccntr  9998  fzaddel  10056  elfzomelpfzo  10228  seq3f1olemstep  10498  seq3f1olemp  10499  sumeq1  11358  summodclem2  11385  summodc  11386  zsumdc  11387  prodmodclem2  11580  prodmodc  11581  divalglemnn  11917  divalglemeunn  11920  divalglemeuneg  11922  dfgcd2  12009  pythagtriplem18  12275  pythagtriplem19  12276  ctiunct  12435  ssomct  12440  isstruct2im  12466  isstruct2r  12467  ptex  12707  isringd  13213  issubrg3  13368  fiinopn  13435  lmfval  13623  upxp  13703  2irrexpqap  14327  dceqnconst  14727  dcapnconst  14728
  Copyright terms: Public domain W3C validator