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

Theorem 3anbi3d 1445
Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
Hypothesis
Ref Expression
3anbi1d.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
3anbi3d (𝜑 → ((𝜃𝜏𝜓) ↔ (𝜃𝜏𝜒)))

Proof of Theorem 3anbi3d
StepHypRef Expression
1 biidd 252 . 2 (𝜑 → (𝜃𝜃))
2 3anbi1d.1 . 2 (𝜑 → (𝜓𝜒))
31, 23anbi13d 1441 1 (𝜑 → ((𝜃𝜏𝜓) ↔ (𝜃𝜏𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  ceqsex3v  3277  ceqsex4v  3278  ceqsex8v  3280  vtocl3gaf  3306  mob  3421  offval22  7298  smogt  7509  cfsmolem  9130  fseq1m1p1  12453  2swrd1eqwrdeq  13500  2swrd2eqwrdeq  13742  wrdl3s3  13751  prodmo  14710  fprod  14715  divalg  15173  funcres2b  16604  posi  16997  mhmlem  17582  isdrngrd  18821  lmodlema  18916  connsub  21272  lmmbr3  23104  lmmcvg  23105  dvmptfsum  23783  axtg5seg  25409  axtgupdim2  25415  axtgeucl  25416  ishlg  25542  hlcomb  25543  brbtwn  25824  axlowdim  25886  axeuclidlem  25887  usgr2wlkspth  26711  usgr2pth0  26717  wwlksnwwlksnon  26878  wwlksnwwlksnonOLD  26880  umgrwwlks2on  26923  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  nvi  27597  isslmd  29883  slmdlema  29884  inelsros  30369  diffiunisros  30370  hgt749d  30855  tgoldbachgt  30869  axtgupdim2OLD  30874  afsval  30877  brafs  30878  bnj981  31146  bnj1326  31220  cvmlift3lem2  31428  cvmlift3lem4  31430  cvmlift3  31436  noprefixmo  31973  nosupno  31974  nosupfv  31977  brofs  32237  brifs  32275  cgr3permute1  32280  brcolinear2  32290  colineardim1  32293  brfs  32311  btwnconn1  32333  brsegle  32340  unblimceq0  32623  unbdqndv2  32627  rdgeqoa  33348  iscringd  33927  oposlem  34787  ishlat1  34957  3dim1lem5  35070  lvoli2  35185  cdlemk42  36546  diclspsn  36800  monotoddzz  37825  jm2.27  37892  mendlmod  38080  fiiuncl  39548  wessf1ornlem  39685  infleinf  39901  fmulcl  40131  fmuldfeqlem1  40132  fmuldfeq  40133  climinf2mpt  40264  climinfmpt  40265  fprodcncf  40432  dvnmptdivc  40471  dvnprodlem2  40480  dvnprodlem3  40481  stoweidlem6  40541  stoweidlem8  40543  stoweidlem26  40561  stoweidlem31  40566  stoweidlem62  40597  fourierdlem41  40683  fourierdlem48  40689  fourierdlem49  40690  sge0iunmpt  40953  ovnsubaddlem1  41105  pfxsuff1eqwrdeq  41732  isgbe  41964  9gbo  41987  11gbo  41988  sbgoldbst  41991  sbgoldbaltlem1  41992  sbgoldbaltlem2  41993  bgoldbtbndlem4  42021  bgoldbtbnd  42022
  Copyright terms: Public domain W3C validator