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

Theorem 3anbi12d 1549
Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
Hypotheses
Ref Expression
3anbi12d.1 (𝜑 → (𝜓𝜒))
3anbi12d.2 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
3anbi12d (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜂)))

Proof of Theorem 3anbi12d
StepHypRef Expression
1 3anbi12d.1 . 2 (𝜑 → (𝜓𝜒))
2 3anbi12d.2 . 2 (𝜑 → (𝜃𝜏))
3 biidd 252 . 2 (𝜑 → (𝜂𝜂))
41, 2, 33anbi123d 1548 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:  3anbi1d  1552  3anbi2d  1553  f1dom3el3dif  6690  fseq1m1p1  12628  dfrtrcl2  14021  imasdsval  16397  iscatd2  16563  ispos  17168  psgnunilem1  18133  ringpropd  18802  mdetunilem3  20642  mdetunilem9  20648  dvfsumlem2  24009  istrkge  25576  axtg5seg  25584  axtgeucl  25591  iscgrad  25923  axlowdim  26061  axeuclid  26063  eengtrkge  26086  umgrvad2edg  26325  upgr3v3e3cycl  27353  upgr4cycl4dv4e  27358  lt2addrd  29846  xlt2addrd  29853  sigaval  30503  issgon  30516  brafs  31080  etasslt  32247  brofs  32439  funtransport  32465  fvtransport  32466  brifs  32477  ifscgr  32478  brcgr3  32480  cgr3permute3  32481  brfs  32513  btwnconn1lem11  32531  funray  32574  fvray  32575  funline  32576  fvline  32578  lpolsetN  37291  rmydioph  38101  iunrelexpmin2  38524
  Copyright terms: Public domain W3C validator