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

Theorem 3anbi3d 1402
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 1398 1 (𝜑 → ((𝜃𝜏𝜓) ↔ (𝜃𝜏𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  ceqsex3v  3232  ceqsex4v  3233  ceqsex8v  3235  vtocl3gaf  3261  mob  3370  offval22  7198  smogt  7409  cfsmolem  9036  fseq1m1p1  12356  2swrd1eqwrdeq  13392  2swrd2eqwrdeq  13630  wrdl3s3  13639  prodmo  14591  fprod  14596  divalg  15050  funcres2b  16478  posi  16871  mhmlem  17456  isdrngrd  18694  lmodlema  18789  connsub  21134  lmmbr3  22966  lmmcvg  22967  dvmptfsum  23642  axtg5seg  25264  axtgupdim2  25270  axtgeucl  25271  ishlg  25397  hlcomb  25398  brbtwn  25679  axlowdim  25741  axeuclidlem  25742  usgr2wlkspth  26524  usgr2pth0  26530  wwlksnwwlksnon  26679  umgrwwlks2on  26719  upgr3v3e3cycl  26906  upgr4cycl4dv4e  26911  nvi  27318  isslmd  29540  slmdlema  29541  inelsros  30022  diffiunisros  30023  axtgupdim2OLD  30453  afsval  30456  brafs  30457  bnj981  30728  bnj1326  30802  cvmlift3lem2  31010  cvmlift3lem4  31012  cvmlift3  31018  frrlem1  31481  noprefixmo  31573  nosino  31575  nosifv  31576  brofs  31754  brifs  31792  cgr3permute1  31797  brcolinear2  31807  colineardim1  31810  brfs  31828  btwnconn1  31850  brsegle  31857  unblimceq0  32140  unbdqndv2  32144  rdgeqoa  32850  iscringd  33429  oposlem  33949  ishlat1  34119  3dim1lem5  34232  lvoli2  34347  cdlemk42  35709  diclspsn  35963  monotoddzz  36988  jm2.27  37055  mendlmod  37244  fiiuncl  38719  wessf1ornlem  38845  infleinf  39052  fmulcl  39217  fmuldfeqlem1  39218  fmuldfeq  39219  climinf2mpt  39350  climinfmpt  39351  fprodcncf  39418  dvnmptdivc  39459  dvnprodlem2  39468  dvnprodlem3  39469  stoweidlem6  39530  stoweidlem8  39532  stoweidlem26  39550  stoweidlem31  39555  stoweidlem62  39586  fourierdlem41  39672  fourierdlem48  39678  fourierdlem49  39679  sge0iunmpt  39942  ovnsubaddlem1  40091  pfxsuff1eqwrdeq  40706  isgbe  40934  9gboa  40957  11gboa  40958  bgoldbst  40961  sgoldbaltlem1  40962  sgoldbaltlem2  40963  bgoldbtbndlem4  40985  bgoldbtbnd  40986
  Copyright terms: Public domain W3C validator