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

Theorem 3anbi3d 1554
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 1550 1 (𝜑 → ((𝜃𝜏𝜓) ↔ (𝜃𝜏𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1072
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 1074
This theorem is referenced by:  ceqsex3v  3386  ceqsex4v  3387  ceqsex8v  3389  vtocl3gaf  3415  mob  3529  offval22  7421  smogt  7633  cfsmolem  9284  fseq1m1p1  12608  2swrd1eqwrdeq  13654  2swrd2eqwrdeq  13897  wrdl3s3  13906  prodmo  14865  fprod  14870  divalg  15328  funcres2b  16758  posi  17151  mhmlem  17736  isdrngrd  18975  lmodlema  19070  connsub  21426  lmmbr3  23258  lmmcvg  23259  dvmptfsum  23937  axtg5seg  25563  axtgupdim2  25569  axtgeucl  25570  ishlg  25696  hlcomb  25697  brbtwn  25978  axlowdim  26040  axeuclidlem  26041  usgr2wlkspth  26865  usgr2pth0  26871  wwlksnwwlksnon  27033  wwlksnwwlksnonOLD  27035  umgrwwlks2on  27078  upgr3v3e3cycl  27332  upgr4cycl4dv4e  27337  nvi  27778  isslmd  30064  slmdlema  30065  inelsros  30550  diffiunisros  30551  hgt749d  31036  tgoldbachgt  31050  axtgupdim2OLD  31055  afsval  31058  brafs  31059  bnj981  31327  bnj1326  31401  cvmlift3lem2  31609  cvmlift3lem4  31611  cvmlift3  31617  noprefixmo  32154  nosupno  32155  nosupfv  32158  brofs  32418  brifs  32456  cgr3permute1  32461  brcolinear2  32471  colineardim1  32474  brfs  32492  btwnconn1  32514  brsegle  32521  unblimceq0  32804  unbdqndv2  32808  rdgeqoa  33529  iscringd  34110  oposlem  34972  ishlat1  35142  3dim1lem5  35255  lvoli2  35370  cdlemk42  36731  diclspsn  36985  monotoddzz  38010  jm2.27  38077  mendlmod  38265  fiiuncl  39733  wessf1ornlem  39870  infleinf  40086  fmulcl  40316  fmuldfeqlem1  40317  fmuldfeq  40318  climinf2mpt  40449  climinfmpt  40450  fprodcncf  40617  dvnmptdivc  40656  dvnprodlem2  40665  dvnprodlem3  40666  stoweidlem6  40726  stoweidlem8  40728  stoweidlem26  40746  stoweidlem31  40751  stoweidlem62  40782  fourierdlem41  40868  fourierdlem48  40874  fourierdlem49  40875  sge0iunmpt  41138  ovnsubaddlem1  41290  pfxsuff1eqwrdeq  41917  isgbe  42149  9gbo  42172  11gbo  42173  sbgoldbst  42176  sbgoldbaltlem1  42177  sbgoldbaltlem2  42178  bgoldbtbndlem4  42206  bgoldbtbnd  42207
  Copyright terms: Public domain W3C validator