Theorem 3anbi123d 1168

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

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858

This theorem is referenced by:  3anbi12d 1169  3anbi13d 1170  3anbi23d 1171  sbc3ang 2508  limeq 3669  limeqOLD 3670  abfii3 5653  abfii4 5654  tz9.1 5753  alephval3 6051  fzaddel 7672  sqrlem20 7942  climaddlem1 8374  climmullem6 8385  expcnvlem5 8492  eflegeo 8681  efm1legeo 8683  acdc3 8755  acdc5 8762  subbas 8914  subbas2 8915  ssblex 9133  lmfval 9203  iscau 9214  isgrp 9321  isring 9465  ringi 9466  vci 9499  isvclem 9528  isnvlem 9561  nvi 9565  vacnlem1 9667  sspval 9721  isssp 9722  ajfval 9809  ipdir 9843  siilem2 9853  isps 9988  indexfi 10174  fine 10213  upxp 10225  txcn 10227  homeofval 10234  ishomeo 10235  isfbas 10261  isfil 10266  fipfil2 10272  infi 10280  fbunfip 10282  limfil 10297  isplig 10345  lpni 10347  isass 10363  ismnd2 10392  unmnd 10405  elunop2 11575  hstel 11787  superpos 11926  bnj921 12828  bnj919 12829  bnj971 12860  bnj578 13291  bnj607 13304  bnj873 13317  divalglem10 13705  dfon2lem1 13849  dfon2lem3 13851  dfon2lem7 13855  wfrlem1 13957  wfrlem15 13971  axdense 14027  infi1 14343  ficli 14353  iscst1 14519  islatalg 14531  isprs 14565  dupre1 14584  vecval1b 14794  vecval3b 14795  vri 14834  rcfpfillem3 14930  rcfpfillem4 14931  rcfpfillem5 14932  rcfpfillem6 14933  istopgrp 14971  topgrpi 14972  cntrsetlem 14999  isalg 15068  algi 15074  isded 15083  dedi 15084  dualcat2 15133  ishoma 15136  ishomc 15138  ishomd 15139  ismona 15158  isepia 15168  isfuna 15182  isfunb 15183  issubcat 15193  issubcata 15194  issubcatb 15195  isseg1 15304  isplibg0 15307  isplibg2 15311  isplibg3 15313  elfiun 15369  inficlALT 15372  hscptsscld 15434  2ndcctbss 15478  islocfin 15506  flimcls 15588  fmfnfm 15598  sfcls 15604  filclus 15605  fclsfnflim 15614  flimfnfcls 15615  fcluscnplem 15617  indexa 15753  indexfiOLD 15755  zornn0 15764  fdc 15812  fsumleisumi 15826  fsumleisum 15827  trirn 15834  neificl 15841  caures 15852  iccshftr 15857  iccshftl 15859  iccdil 15861  icccntr 15863  tlmval 15903  sstotbnd 15936  isgrpda 16033  pi1gp 16095  isringd 16097  rnghomval 16118  isrnghom 16119  igenval2 16214  smoeq 16444  stb3xpl 16743  isposNEW 16773  poslem 16774  isopos 16909  oposlem 16913  cmtfval 16937  cvrfval 16987  isringNEW 17142  ringiNEW 17143  issrng 17176  islvec 17188  isphil 17195

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 164  df-an 242  df-3an 860

Copyright terms: Public domain