Theorem 3anbi123d 890

Description: Deduction joining 3 equivalences to form equivalence of conjunctions.

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 626	. . 3 |- (ph -> ((ps /\ th) <-> (ch /\ ta)))
4		bi3d.3	. . 3 |- (ph -> (et <-> ze))
5	3, 4	anbi12d 626	. 2 |- (ph -> (((ps /\ th) /\ et) <-> ((ch /\ ta) /\ ze)))
6		df-3an 775	. 2 |- ((ps /\ th /\ et) <-> ((ps /\ th) /\ et))
7		df-3an 775	. 2 |- ((ch /\ ta /\ ze) <-> ((ch /\ ta) /\ ze))
8	5, 6, 7	3bitr4g 553	1 |- (ph -> ((ps /\ th /\ et) <-> (ch /\ ta /\ ze)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   /\ w3a 773

This theorem is referenced by:  3anbi12d 891  3anbi13d 892  3anbi23d 893  limeq 2950  abfii3 4537  abfii4 4538  tz9.1 4618  alephval3 4875  fzaddelt 6432  sqrlem20 6622  climaddlem1 7050  climmullem6 7061  expcnvlem5 7166  eflegeot 7356  efm1legeot 7358  acdc3 7429  acdc5 7435  subbas 7586  subbas2 7587  ssblex 7796  lmfval 7863  iscau 7874  isgrp 7975  isring 8078  ringi 8079  vci 8104  isvcgOLD 8133  isvclem 8134  isnvlem 8167  isnvgOLD 8168  nvi 8173  sspval 8316  isssp 8317  ajfval 8400  ipdir 8433  siilem2 8443  isps 8571  elunop2t 9853  hstelt 10052  superpos 10189  infi1 10347  fine 10348  ficli 10368  homeofval 10403  ishomeo 10404  isfil 10433  fipfil2 10439  infi 10448  isalg 10497  algi 10504  isded 10513  dedi 10514  ishoma 10559  ishomb 10560  ishomc 10561  ishomd 10562  ismona 10579  isfuna 10592  isfunb 10593

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 775

Copyright terms: Public domain