Theorem 3anbi123d 1325

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 983	. 2 |- ( ( ps /\ th /\ et ) <-> ( ( ps /\ th ) /\ et ) )
7		df-3an 983	. 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 981

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 983

This theorem is referenced by:  3anbi12d  1326  3anbi13d  1327  3anbi23d  1328  limeq  4442  smoeq  6399  tfrlemi1  6441  tfr1onlemaccex  6457  tfrcllemaccex  6470  ereq1  6650  updjud  7210  ctssdclemr  7240  tapeq1  7399  tapeq2  7400  elinp  7622  sup3exmid  9065  iccshftr  10151  iccshftl  10153  iccdil  10155  icccntr  10157  fzaddel  10216  elfzomelpfzo  10397  seq3f1olemstep  10696  seq3f1olemp  10697  wrdl1s1  11122  sumeq1  11781  summodclem2  11808  summodc  11809  zsumdc  11810  prodmodclem2  12003  prodmodc  12004  divalglemnn  12344  divalglemeunn  12347  divalglemeuneg  12349  dfgcd2  12450  pythagtriplem18  12719  pythagtriplem19  12720  ctiunct  12926  ssomct  12931  isstruct2im  12957  isstruct2r  12958  ptex  13211  imasmnd2  13399  imasgrp2  13561  isrngd  13830  imasrng  13833  isringd  13918  imasring  13941  subrngpropd  14093  issubrg3  14124  islmod  14168  lmodlema  14169  islmodd  14170  lmodprop2d  14225  fiinopn  14591  lmfval  14779  upxp  14859  ivthdich  15240  2irrexpqap  15565  dceqnconst  16201  dcapnconst  16202