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

Theorem 3anbi12d 1548
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 1547 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜂)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  3anbi1d  1551  3anbi2d  1552  f1dom3el3dif  6668  fseq1m1p1  12618  dfrtrcl2  14006  imasdsval  16379  iscatd2  16545  ispos  17151  psgnunilem1  18116  ringpropd  18786  mdetunilem3  20634  mdetunilem9  20640  dvfsumlem2  24006  istrkge  25573  axtg5seg  25581  axtgeucl  25588  iscgrad  25920  axlowdim  26058  axeuclid  26060  eengtrkge  26083  umgrvad2edg  26323  upgr3v3e3cycl  27356  upgr4cycl4dv4e  27361  lt2addrd  29852  xlt2addrd  29859  sigaval  30509  issgon  30522  brafs  31086  etasslt  32253  brofs  32445  funtransport  32471  fvtransport  32472  brifs  32483  ifscgr  32484  brcgr3  32486  cgr3permute3  32487  brfs  32519  btwnconn1lem11  32537  funray  32580  fvray  32581  funline  32582  fvline  32584  lpolsetN  37289  rmydioph  38104  iunrelexpmin2  38527
  Copyright terms: Public domain W3C validator