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

Theorem 3anbi13d 1441
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 252 . 2 (𝜑 → (𝜂𝜂))
3 3anbi12d.2 . 2 (𝜑 → (𝜃𝜏))
41, 2, 33anbi123d 1439 1 (𝜑 → ((𝜓𝜂𝜃) ↔ (𝜒𝜂𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1054
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 1056
This theorem is referenced by:  3anbi3d  1445  ax12wdemo  2052  f1dom3el3dif  6566  wfrlem1  7459  wfrlem3a  7462  wfrlem15  7474  cofsmo  9129  axdc3lem3  9312  axdc3lem4  9313  iscatd2  16389  psgnunilem1  17959  nn0gsumfz  18426  opprsubrg  18849  lsspropd  19065  mdetunilem3  20468  mdetunilem9  20474  smadiadetr  20529  lmres  21152  cnhaus  21206  regsep2  21228  dishaus  21234  ordthauslem  21235  nconnsubb  21274  pthaus  21489  txhaus  21498  xkohaus  21504  regr1lem  21590  ustval  22053  methaus  22372  metnrmlem3  22711  pmltpclem1  23263  axtgeucl  25416  iscgrad  25748  dfcgra2  25766  f1otrge  25797  axeuclidlem  25887  umgrvad2edg  26150  elwspths2spth  26934  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  vdgn1frgrv2  27276  ex-opab  27419  isnvlem  27593  ajval  27845  adjeu  28876  adjval  28877  adj1  28920  adjeq  28922  cnlnssadj  29067  br8d  29548  lt2addrd  29644  xlt2addrd  29651  measval  30389  br8  31772  br6  31773  br4  31774  frrlem1  31905  brsslt  32025  brcgr3  32278  brsegle  32340  fvray  32373  linedegen  32375  fvline  32376  poimirlem28  33567  isopos  34785  hlsuprexch  34985  2llnjN  35171  2lplnj  35224  cdlemk42  36546  zindbi  37828  jm2.27  37892  stoweidlem43  40578  fourierdlem42  40684
  Copyright terms: Public domain W3C validator