Theorem 3anbi123d 891

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

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

This theorem is referenced by:  3anbi12d 892  3anbi13d 893  3anbi23d 894  limeq 2955  abfii3 4543  abfii4 4544  tz9.1 4626  alephval3 4883  fzaddelt 6440  sqrlem20 6630  climaddlem1 7058  climmullem6 7069  expcnvlem5 7174  eflegeot 7364  efm1legeot 7366  acdc3 7437  acdc5 7443  subbas 7594  subbas2 7595  ssblex 7808  lmfval 7877  iscau 7888  isgrp 7991  isring 8093  ringi 8094  vci 8119  isvclem 8148  isnvlem 8181  nvi 8185  sspval 8329  isssp 8330  ajfval 8413  ipdir 8446  siilem2 8456  isps 8588  elunop2t 9876  hstelt 10080  superpos 10218  infi1 10383  fine 10384  ficli 10404  homeofval 10439  ishomeo 10440  isfil 10469  fipfil2 10475  infi 10484  isalg 10533  algi 10540  isded 10549  dedi 10550  ishoma 10595  ishomb 10596  ishomc 10597  ishomd 10598  ismona 10615  isfuna 10628  isfunb 10629

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 776

Copyright terms: Public domain