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

Theorem 3anbi13d 1400
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 1398 1 (𝜑 → ((𝜓𝜂𝜃) ↔ (𝜒𝜂𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1037
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 386  df-3an 1039
This theorem is referenced by:  3anbi3d  1404  ax12wdemo  2011  f1dom3el3dif  6523  wfrlem1  7411  wfrlem3a  7414  wfrlem15  7426  cofsmo  9088  axdc3lem3  9271  axdc3lem4  9272  iscatd2  16336  psgnunilem1  17907  nn0gsumfz  18374  opprsubrg  18795  lsspropd  19011  mdetunilem3  20414  mdetunilem9  20420  smadiadetr  20475  lmres  21098  cnhaus  21152  regsep2  21174  dishaus  21180  ordthauslem  21181  nconnsubb  21220  pthaus  21435  txhaus  21444  xkohaus  21450  regr1lem  21536  ustval  22000  methaus  22319  metnrmlem3  22658  pmltpclem1  23211  axtgeucl  25365  iscgrad  25697  dfcgra2  25715  f1otrge  25746  axeuclidlem  25836  umgrvad2edg  26099  elwspths2spth  26856  upgr3v3e3cycl  27033  upgr4cycl4dv4e  27038  vdgn1frgrv2  27153  ex-opab  27273  isnvlem  27449  ajval  27701  adjeu  28732  adjval  28733  adj1  28776  adjeq  28778  cnlnssadj  28923  br8d  29406  lt2addrd  29501  xlt2addrd  29508  measval  30246  br8  31632  br6  31633  br4  31634  brsslt  31884  brcgr3  32137  brsegle  32199  fvray  32232  linedegen  32234  fvline  32235  poimirlem28  33417  isopos  34293  hlsuprexch  34493  2llnjN  34679  2lplnj  34732  cdlemk42  36055  zindbi  37337  jm2.27  37401  stoweidlem43  40029  fourierdlem42  40135
  Copyright terms: Public domain W3C validator