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

Theorem 3anbi3d 1439
 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 265 . 2 (𝜑 → (𝜃𝜃))
2 3anbi1d.1 . 2 (𝜑 → (𝜓𝜒))
31, 23anbi13d 1435 1 (𝜑 → ((𝜃𝜏𝜓) ↔ (𝜃𝜏𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  ceqsex3v  3493  ceqsex4v  3494  ceqsex8v  3496  vtocl3gaf  3525  mob  3656  offval22  7768  smogt  7989  cfsmolem  9683  fseq1m1p1  12979  pfxsuff1eqwrdeq  14054  2swrd2eqwrdeq  14308  wrdl3s3  14319  prodmo  15284  fprod  15289  divalg  15746  funcres2b  17161  posi  17554  mhmlem  18214  isdrngrd  19524  lmodlema  19635  connsub  22033  lmmbr3  23871  lmmcvg  23872  dvmptfsum  24585  axtg5seg  26266  axtgupdim2  26272  axtgeucl  26273  ishlg  26403  hlcomb  26404  brbtwn  26700  axlowdim  26762  axeuclidlem  26763  usgr2wlkspth  27555  usgr2pth0  27561  wwlksnwwlksnon  27708  umgrwwlks2on  27750  upgr3v3e3cycl  27972  upgr4cycl4dv4e  27977  nvi  28404  isslmd  30887  slmdlema  30888  inelsros  31559  diffiunisros  31560  hgt749d  32042  tgoldbachgt  32056  axtgupdim2ALTV  32061  afsval  32064  brafs  32065  bnj981  32344  bnj1326  32420  cvmlift3lem2  32692  cvmlift3lem4  32694  cvmlift3  32700  noprefixmo  33327  nosupno  33328  nosupfv  33331  brofs  33591  brifs  33629  cgr3permute1  33634  brcolinear2  33644  colineardim1  33647  brfs  33665  btwnconn1  33687  brsegle  33694  unblimceq0  33971  unbdqndv2  33975  rdgeqoa  34803  iscringd  35452  oposlem  36494  ishlat1  36664  3dim1lem5  36778  lvoli2  36893  cdlemk42  38253  diclspsn  38506  monotoddzz  39899  jm2.27  39964  mendlmod  40152  fiiuncl  41714  wessf1ornlem  41826  infleinf  42019  fmulcl  42238  fmuldfeqlem1  42239  fmuldfeq  42240  climinf2mpt  42371  climinfmpt  42372  fprodcncf  42557  dvnmptdivc  42595  dvnprodlem2  42604  dvnprodlem3  42605  stoweidlem6  42663  stoweidlem8  42665  stoweidlem26  42683  stoweidlem31  42688  stoweidlem62  42719  fourierdlem41  42805  fourierdlem48  42811  fourierdlem49  42812  sge0iunmpt  43072  ovnsubaddlem1  43224  isgbe  44284  9gbo  44307  11gbo  44308  sbgoldbst  44311  sbgoldbaltlem1  44312  sbgoldbaltlem2  44313  bgoldbtbndlem4  44341  bgoldbtbnd  44342
 Copyright terms: Public domain W3C validator