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

Step	Hyp	Ref	Expression
1		bi3d.1	. . . 4 |- ( ph -> ( ps <-> ch ) )
2		bi3d.2	. . . 4 |- ( ph -> ( th <-> ta ) )
3	1, 2	anbi12d 473	. . 3 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ ta ) ) )
4		bi3d.3	. . 3 |- ( ph -> ( et <-> ze ) )
5	3, 4	anbi12d 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 ) )
8	5, 6, 7	3bitr4g 223	1 |- ( ph -> ( ( ps /\ th /\ et ) <-> ( ch /\ ta /\ ze ) ) )

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