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

Theorem 3anbi12d 1391
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 250 . 2 (𝜑 → (𝜂𝜂))
41, 2, 33anbi123d 1390 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜂)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  3anbi1d  1394  3anbi2d  1395  f1dom3el3dif  6404  fseq1m1p1  12242  dfrtrcl2  13599  imasdsval  15947  iscatd2  16114  ispos  16719  psgnunilem1  17685  ringpropd  18354  mdetunilem3  20187  mdetunilem9  20193  dvfsumlem2  23539  istrkge  25101  axtg5seg  25109  axtgeucl  25116  iscgrad  25449  axlowdim  25587  axeuclid  25589  eengtrkge  25612  lt2addrd  28737  xlt2addrd  28747  sigaval  29334  issgon  29347  brafs  29837  brofs  31116  funtransport  31142  fvtransport  31143  brifs  31154  ifscgr  31155  brcgr3  31157  cgr3permute3  31158  brfs  31190  btwnconn1lem11  31208  funray  31251  fvray  31252  funline  31253  fvline  31255  lpolsetN  35613  rmydioph  36423  iunrelexpmin2  36847  umgrvad2edg  40462  upgr3v3e3cycl  41369  upgr4cycl4dv4e  41374
  Copyright terms: Public domain W3C validator