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

Theorem 3anbi13d 1392
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
3anbi13d (𝜑 → ((𝜓𝜂𝜃) ↔ (𝜒𝜂𝜏)))

Proof of Theorem 3anbi13d
StepHypRef Expression
1 3anbi12d.1 . 2 (𝜑 → (𝜓𝜒))
2 biidd 250 . 2 (𝜑 → (𝜂𝜂))
3 3anbi12d.2 . 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:  3anbi3d  1396  ax12wdemo  1998  f1dom3el3dif  6404  wfrlem1  7279  wfrlem3a  7282  wfrlem15  7294  cofsmo  8952  axdc3lem3  9135  axdc3lem4  9136  iscatd2  16114  psgnunilem1  17685  nn0gsumfz  18152  opprsubrg  18573  lsspropd  18787  mdetunilem3  20187  mdetunilem9  20193  smadiadetr  20248  lmres  20862  cnhaus  20916  regsep2  20938  dishaus  20944  ordthauslem  20945  nconsubb  20984  pthaus  21199  txhaus  21208  xkohaus  21214  regr1lem  21300  ustval  21764  methaus  22083  metnrmlem3  22420  pmltpclem1  22969  axtgeucl  25116  iscgrad  25449  dfcgra2  25467  f1otrge  25498  axeuclidlem  25588  2wlkonot  26186  2spthonot  26187  usg2spthonot0  26210  vdn0frgrav2  26344  vdgn0frgrav2  26345  vdn1frgrav2  26346  vdgn1frgrav2  26347  ex-opab  26475  isnvlem  26661  ajval  26935  adjeu  27966  adjval  27967  adj1  28010  adjeq  28012  cnlnssadj  28157  br8d  28636  lt2addrd  28737  xlt2addrd  28747  measval  29422  br8  30733  br6  30734  br4  30735  nofulllem5  30939  brcgr3  31157  brsegle  31219  fvray  31252  linedegen  31254  fvline  31255  poimirlem28  32431  isopos  33309  hlsuprexch  33509  2llnjN  33695  2lplnj  33748  cdlemk42  35071  zindbi  36353  jm2.27  36417  stoweidlem43  38760  fourierdlem42  38866  umgrvad2edg  40462  elwspths2spth  41193  upgr3v3e3cycl  41369  upgr4cycl4dv4e  41374  vdgn1frgrv2  41488
  Copyright terms: Public domain W3C validator