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

Theorem 3anbi3d 1566
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 253 . 2 (𝜑 → (𝜃𝜃))
2 3anbi1d.1 . 2 (𝜑 → (𝜓𝜒))
31, 23anbi13d 1562 1 (𝜑 → ((𝜃𝜏𝜓) ↔ (𝜃𝜏𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  ceqsex3v  3399  ceqsex4v  3400  ceqsex8v  3402  vtocl3gaf  3427  mob  3547  offval22  7455  smogt  7668  cfsmolem  9345  fseq1m1p1  12622  2swrd1eqwrdeqOLD  13656  pfxsuff1eqwrdeq  13686  2swrd2eqwrdeq  13984  2swrd2eqwrdeqOLD  13985  wrdl3s3  13994  prodmo  14951  fprod  14956  divalg  15410  funcres2b  16824  posi  17218  mhmlem  17804  isdrngrd  19042  lmodlema  19137  connsub  21504  lmmbr3  23337  lmmcvg  23338  dvmptfsum  24029  axtg5seg  25655  axtgupdim2  25661  axtgeucl  25662  ishlg  25788  hlcomb  25789  brbtwn  26070  axlowdim  26132  axeuclidlem  26133  usgr2wlkspth  26946  usgr2pth0  26952  wwlksnwwlksnon  27116  wwlksnwwlksnonOLD  27118  umgrwwlks2on  27161  upgr3v3e3cycl  27416  upgr4cycl4dv4e  27421  nvi  27860  isslmd  30137  slmdlema  30138  inelsros  30623  diffiunisros  30624  hgt749d  31110  tgoldbachgt  31124  axtgupdim2OLD  31129  afsval  31132  brafs  31133  bnj981  31400  bnj1326  31474  cvmlift3lem2  31682  cvmlift3lem4  31684  cvmlift3  31690  noprefixmo  32224  nosupno  32225  nosupfv  32228  brofs  32488  brifs  32526  cgr3permute1  32531  brcolinear2  32541  colineardim1  32544  brfs  32562  btwnconn1  32584  brsegle  32591  unblimceq0  32869  unbdqndv2  32873  rdgeqoa  33583  iscringd  34151  oposlem  35070  ishlat1  35240  3dim1lem5  35354  lvoli2  35469  cdlemk42  36829  diclspsn  37082  monotoddzz  38117  jm2.27  38184  mendlmod  38372  fiiuncl  39817  wessf1ornlem  39950  infleinf  40158  fmulcl  40383  fmuldfeqlem1  40384  fmuldfeq  40385  climinf2mpt  40516  climinfmpt  40517  fprodcncf  40684  dvnmptdivc  40723  dvnprodlem2  40732  dvnprodlem3  40733  stoweidlem6  40792  stoweidlem8  40794  stoweidlem26  40812  stoweidlem31  40817  stoweidlem62  40848  fourierdlem41  40934  fourierdlem48  40940  fourierdlem49  40941  sge0iunmpt  41204  ovnsubaddlem1  41356  isgbe  42247  9gbo  42270  11gbo  42271  sbgoldbst  42274  sbgoldbaltlem1  42275  sbgoldbaltlem2  42276  bgoldbtbndlem4  42304  bgoldbtbnd  42305
  Copyright terms: Public domain W3C validator