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  4378  smoeq  6291  tfrlemi1  6333  tfr1onlemaccex  6349  tfrcllemaccex  6362  ereq1  6542  updjud  7081  ctssdclemr  7111  tapeq1  7251  tapeq2  7252  elinp  7473  sup3exmid  8914  iccshftr  9994  iccshftl  9996  iccdil  9998  icccntr  10000  fzaddel  10059  elfzomelpfzo  10231  seq3f1olemstep  10501  seq3f1olemp  10502  sumeq1  11363  summodclem2  11390  summodc  11391  zsumdc  11392  prodmodclem2  11585  prodmodc  11586  divalglemnn  11923  divalglemeunn  11926  divalglemeuneg  11928  dfgcd2  12015  pythagtriplem18  12281  pythagtriplem19  12282  ctiunct  12441  ssomct  12446  isstruct2im  12472  isstruct2r  12473  ptex  12713  isringd  13220  issubrg3  13368  islmod  13381  lmodlema  13382  islmodd  13383  lmodprop2d  13438  fiinopn  13507  lmfval  13695  upxp  13775  2irrexpqap  14399  dceqnconst  14810  dcapnconst  14811