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

Theorem 3anbi13d 1555
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 253 . 2 (𝜑 → (𝜂𝜂))
3 3anbi12d.2 . 2 (𝜑 → (𝜃𝜏))
41, 2, 33anbi123d 1553 1 (𝜑 → ((𝜓𝜂𝜃) ↔ (𝜒𝜂𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  3anbi3d  1559  ax12wdemo  2178  f1dom3el3dif  6746  wfrlem1  7645  wfrlem3a  7648  wfrlem15  7661  cofsmo  9372  axdc3lem3  9555  axdc3lem4  9556  iscatd2  16542  psgnunilem1  18110  nn0gsumfz  18577  opprsubrg  19001  lsspropd  19220  mdetunilem3  20628  mdetunilem9  20634  smadiadetr  20690  lmres  21315  cnhaus  21369  regsep2  21391  dishaus  21397  ordthauslem  21398  nconnsubb  21437  pthaus  21652  txhaus  21661  xkohaus  21667  regr1lem  21753  ustval  22216  methaus  22535  metnrmlem3  22874  pmltpclem1  23428  axtgeucl  25584  iscgrad  25916  dfcgra2  25934  f1otrge  25965  axeuclidlem  26055  umgrvad2edg  26319  elwspths2spth  27108  upgr3v3e3cycl  27352  upgr4cycl4dv4e  27357  vdgn1frgrv2  27470  numclwlk1lem1  27548  ex-opab  27619  isnvlem  27792  ajval  28044  adjeu  29075  adjval  29076  adj1  29119  adjeq  29121  cnlnssadj  29266  br8d  29746  lt2addrd  29842  xlt2addrd  29849  measval  30585  br8  31966  br6  31967  br4  31968  frrlem1  32099  brsslt  32219  brcgr3  32472  brsegle  32534  fvray  32567  linedegen  32569  fvline  32570  poimirlem28  33748  isopos  34958  hlsuprexch  35159  2llnjN  35345  2lplnj  35398  cdlemk42  36719  zindbi  38009  jm2.27  38073  stoweidlem43  40736  fourierdlem42  40842
  Copyright terms: Public domain W3C validator