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

Theorem 3anbi3d 1442
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 261 . 2 (𝜑 → (𝜃𝜃))
2 3anbi1d.1 . 2 (𝜑 → (𝜓𝜒))
31, 23anbi13d 1438 1 (𝜑 → ((𝜃𝜏𝜓) ↔ (𝜃𝜏𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  ceqsex3v  3498  ceqsex4v  3499  ceqsex8v  3501  vtocl3gaf  3535  vtocl3ga  3536  mob  3673  offval22  8016  smogt  8309  ttrcleq  9641  cfsmolem  10202  fseq1m1p1  13508  pfxsuff1eqwrdeq  14579  2swrd2eqwrdeq  14834  wrdl3s3  14843  prodmo  15811  fprod  15816  divalg  16277  funcres2b  17775  posi  18198  mhmlem  18858  isdrngrd  20200  lmodlema  20312  connsub  22756  lmmbr3  24608  lmmcvg  24609  dvmptfsum  25323  nosupprefixmo  27032  noinfprefixmo  27033  nosupcbv  27034  nosupno  27035  nosupfv  27038  noinfcbv  27049  noinfno  27050  noinffv  27053  axtg5seg  27293  axtgupdim2  27299  axtgeucl  27300  ishlg  27430  hlcomb  27431  brbtwn  27734  axlowdim  27796  axeuclidlem  27797  usgr2wlkspth  28593  usgr2pth0  28599  wwlksnwwlksnon  28746  umgrwwlks2on  28788  upgr3v3e3cycl  29010  upgr4cycl4dv4e  29015  nvi  29442  isslmd  31920  slmdlema  31921  inelsros  32646  diffiunisros  32647  hgt749d  33131  tgoldbachgt  33145  axtgupdim2ALTV  33150  afsval  33153  brafs  33154  bnj981  33431  bnj1326  33507  cvmlift3lem2  33783  cvmlift3lem4  33785  cvmlift3  33791  brofs  34557  brifs  34595  cgr3permute1  34600  brcolinear2  34610  colineardim1  34613  brfs  34631  btwnconn1  34653  brsegle  34660  unblimceq0  34937  unbdqndv2  34941  rdgeqoa  35808  iscringd  36424  oposlem  37611  ishlat1  37781  3dim1lem5  37896  lvoli2  38011  cdlemk42  39371  diclspsn  39624  monotoddzz  41205  jm2.27  41270  mendlmod  41458  fiiuncl  43215  wessf1ornlem  43339  infleinf  43542  fmulcl  43754  fmuldfeqlem1  43755  fmuldfeq  43756  climinf2mpt  43887  climinfmpt  43888  fprodcncf  44073  dvnmptdivc  44111  dvnprodlem2  44120  dvnprodlem3  44121  stoweidlem6  44179  stoweidlem8  44181  stoweidlem26  44199  stoweidlem31  44204  stoweidlem62  44235  fourierdlem41  44321  fourierdlem48  44327  fourierdlem49  44328  sge0iunmpt  44591  ovnsubaddlem1  44743  isgbe  45875  9gbo  45898  11gbo  45899  sbgoldbst  45902  sbgoldbaltlem1  45903  sbgoldbaltlem2  45904  bgoldbtbndlem4  45932  bgoldbtbnd  45933
  Copyright terms: Public domain W3C validator