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

Theorem 3anbi3d 1443
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 262 . 2 (𝜑 → (𝜃𝜃))
2 3anbi1d.1 . 2 (𝜑 → (𝜓𝜒))
31, 23anbi13d 1439 1 (𝜑 → ((𝜃𝜏𝜓) ↔ (𝜃𝜏𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  ceqsex3v  3499  ceqsex4v  3500  ceqsex8v  3502  vtocl3gaf  3536  vtocl3ga  3537  mob  3676  offval22  8021  smogt  8314  ttrcleq  9650  cfsmolem  10211  fseq1m1p1  13522  pfxsuff1eqwrdeq  14593  2swrd2eqwrdeq  14848  wrdl3s3  14857  prodmo  15824  fprod  15829  divalg  16290  funcres2b  17788  posi  18211  mhmlem  18872  isdrngrd  20227  isdrngrdOLD  20229  lmodlema  20341  connsub  22788  lmmbr3  24640  lmmcvg  24641  dvmptfsum  25355  nosupprefixmo  27064  noinfprefixmo  27065  nosupcbv  27066  nosupno  27067  nosupfv  27070  noinfcbv  27081  noinfno  27082  noinffv  27085  axtg5seg  27449  axtgupdim2  27455  axtgeucl  27456  ishlg  27586  hlcomb  27587  brbtwn  27890  axlowdim  27952  axeuclidlem  27953  usgr2wlkspth  28749  usgr2pth0  28755  wwlksnwwlksnon  28902  umgrwwlks2on  28944  upgr3v3e3cycl  29166  upgr4cycl4dv4e  29171  nvi  29598  isslmd  32086  slmdlema  32087  inelsros  32834  diffiunisros  32835  hgt749d  33319  tgoldbachgt  33333  axtgupdim2ALTV  33338  afsval  33341  brafs  33342  bnj981  33619  bnj1326  33695  cvmlift3lem2  33971  cvmlift3lem4  33973  cvmlift3  33979  brofs  34636  brifs  34674  cgr3permute1  34679  brcolinear2  34689  colineardim1  34692  brfs  34710  btwnconn1  34732  brsegle  34739  unblimceq0  35016  unbdqndv2  35020  rdgeqoa  35887  iscringd  36503  oposlem  37690  ishlat1  37860  3dim1lem5  37975  lvoli2  38090  cdlemk42  39450  diclspsn  39703  monotoddzz  41310  jm2.27  41375  mendlmod  41563  fiiuncl  43361  wessf1ornlem  43491  infleinf  43693  fmulcl  43908  fmuldfeqlem1  43909  fmuldfeq  43910  climinf2mpt  44041  climinfmpt  44042  fprodcncf  44227  dvnmptdivc  44265  dvnprodlem2  44274  dvnprodlem3  44275  stoweidlem6  44333  stoweidlem8  44335  stoweidlem26  44353  stoweidlem31  44358  stoweidlem62  44389  fourierdlem41  44475  fourierdlem48  44481  fourierdlem49  44482  sge0iunmpt  44745  ovnsubaddlem1  44897  isgbe  46029  9gbo  46052  11gbo  46053  sbgoldbst  46056  sbgoldbaltlem1  46057  sbgoldbaltlem2  46058  bgoldbtbndlem4  46086  bgoldbtbnd  46087
  Copyright terms: Public domain W3C validator