MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anbi23d Structured version   Visualization version   GIF version

Theorem 3anbi23d 1399
Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
Hypotheses
Ref Expression
3anbi12d.1 (𝜑 → (𝜓𝜒))
3anbi12d.2 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
3anbi23d (𝜑 → ((𝜂𝜓𝜃) ↔ (𝜂𝜒𝜏)))

Proof of Theorem 3anbi23d
StepHypRef Expression
1 biidd 252 . 2 (𝜑 → (𝜂𝜂))
2 3anbi12d.1 . 2 (𝜑 → (𝜓𝜒))
3 3anbi12d.2 . 2 (𝜑 → (𝜃𝜏))
41, 2, 33anbi123d 1396 1 (𝜑 → ((𝜂𝜓𝜃) ↔ (𝜂𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038
This theorem is referenced by:  f1dom3el3dif  6480  wrecseq123  7353  oeeui  7627  fpwwe2lem5  9400  pwfseqlem4a  9427  pwfseqlem4  9428  swrdccatin12lem3  13427  prodeq2w  14567  prodeq2ii  14568  divalg  15050  dfgcd2  15187  iscatd2  16263  posi  16871  issubg3  17533  pmtrfrn  17799  psgnunilem2  17836  psgnunilem3  17837  lmhmpropd  18992  lbsacsbs  19075  frlmphl  20039  neiptoptop  20845  neiptopnei  20846  cnhaus  21068  nrmsep  21071  dishaus  21096  ordthauslem  21097  nconnsubb  21136  pthaus  21351  txhaus  21360  xkohaus  21366  regr1lem  21452  isust  21917  ustuqtop4  21958  methaus  22235  metnrmlem3  22572  iscau4  22985  pmltpclem1  23124  dvfsumlem2  23694  aannenlem1  23987  aannenlem2  23988  istrkgcb  25255  hlbtwn  25406  iscgra  25601  dfcgra2  25621  f1otrge  25652  axlowdim  25741  axeuclidlem  25742  eengtrkg  25765  clwwlks  26746  clwlkclwwlk  26770  clwlksfclwwlk  26828  upgr3v3e3cycl  26906  upgr4cycl4dv4e  26911  numclwwlk5  27100  ex-opab  27143  l2p  27184  vciOLD  27265  isvclem  27281  isnvlem  27314  dipass  27549  adj1  28641  adjeq  28643  cnlnssadj  28788  br8d  29265  carsgmon  30157  carsgsigalem  30158  carsgclctunlem2  30162  carsgclctun  30164  bnj1154  30775  br8  31354  br6  31355  br4  31356  fvtransport  31781  brcgr3  31795  brfs  31828  fscgr  31829  btwnconn1lem11  31846  brsegle  31857  fvray  31890  linedegen  31892  fvline  31893  poimirlem28  33069  poimirlem32  33073  heiborlem2  33243  hlsuprexch  34147  3dim1lem5  34232  lplni2  34303  2llnjN  34333  lvoli2  34347  2lplnj  34386  cdleme18d  35062  cdlemg1cex  35356  ismrc  36744  monotoddzzfi  36987  oddcomabszz  36989  zindbi  36991  rmydioph  37061  fsumiunss  39211  sumnnodd  39266  stoweidlem31  39555  stoweidlem34  39558  stoweidlem43  39567  stoweidlem48  39572  fourierdlem42  39673  sge0iunmptlemre  39939  sge0iunmpt  39942  vonioo  40203  vonicc  40206
  Copyright terms: Public domain W3C validator