Theorem 3anbi123d 893

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

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

This theorem is referenced by:  3anbi12d 894  3anbi13d 895  3anbi23d 896  limeq 2960  abfii3OLD 4563  abfii4OLD 4564  tz9.1 4646  alephval3 4903  fzaddelt 6500  sqrlem20 6692  climaddlem1 7114  climmullem6 7125  expcnvlem5 7231  eflegeot 7416  efm1legeot 7418  acdc3 7487  acdc5 7493  subbasOLD 7644  subbas2OLD 7645  ssblex 7856  lmfval 7925  iscau 7936  isgrp 8041  isring 8141  ringi 8142  vci 8167  isvclem 8196  isnvlem 8229  nvi 8233  sspval 8382  isssp 8383  ajfval 8469  ipdir 8502  siilem2 8512  isps 8645  elunop2t 9938  hstelt 10142  superpos 10281  infi1 10447  infi1OLD 10448  fine 10449  fineOLD 10450  ficli 10472  ficliOLD 10473  homeofval 10516  ishomeo 10517  isfil 10558  fipfil2 10564  fipfil2OLD 10565  infi 10578  infiOLD 10579  rcfpfillem3 10589  rcfpfillem3OLD 10590  rcfpfillem4 10591  rcfpfillem4OLD 10592  rcfpfillem5 10593  rcfpfillem5OLD 10594  rcfpfillem6 10595  rcfpfillem6OLD 10596  isalg 10653  algi 10660  isded 10669  dedi 10670  ishoma 10715  ishomb 10716  ishomc 10717  ishomd 10718  ismona 10737  isepia 10747  isepib2 10750  isfuna 10754  isfunb 10755

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 777

Copyright terms: Public domain