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

Theorem 3anbi13d 1438
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 261 . 2 (𝜑 → (𝜂𝜂))
3 3anbi12d.2 . 2 (𝜑 → (𝜃𝜏))
41, 2, 33anbi123d 1436 1 (𝜑 → ((𝜓𝜂𝜃) ↔ (𝜒𝜂𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  3anbi3d  1442  ax12wdemo  2131  f1dom3el3dif  7213  xpord2lem  8071  xpord3lem  8078  frrlem1  8214  frrlem13  8226  wfrlem1OLD  8251  wfrlem3OLDa  8254  wfrlem15OLD  8266  cofsmo  10202  axdc3lem3  10385  axdc3lem4  10386  iscatd2  17558  psgnunilem1  19271  nn0gsumfz  19757  opprsubrg  20239  lsspropd  20474  mdetunilem3  21959  mdetunilem9  21965  smadiadetr  22020  lmres  22647  cnhaus  22701  regsep2  22723  dishaus  22729  ordthauslem  22730  nconnsubb  22770  pthaus  22985  txhaus  22994  xkohaus  23000  regr1lem  23086  ustval  23550  methaus  23872  metnrmlem3  24220  pmltpclem1  24808  brsslt  27121  axtgeucl  27312  iscgrad  27651  dfcgra2  27670  f1otrge  27712  axeuclidlem  27809  umgrvad2edg  28059  elwspths2spth  28810  upgr3v3e3cycl  29022  upgr4cycl4dv4e  29027  vdgn1frgrv2  29138  numclwlk1lem1  29211  ex-opab  29274  isnvlem  29450  ajval  29701  adjeu  30729  adjval  30730  adj1  30773  adjeq  30775  cnlnssadj  30920  br8d  31427  lt2addrd  31551  xlt2addrd  31558  measval  32688  loop1cycl  33622  br8  34221  br6  34222  br4  34223  brcgr3  34620  brsegle  34682  fvray  34715  linedegen  34717  fvline  34718  poimirlem28  36095  isopos  37631  hlsuprexch  37833  2llnjN  38019  2lplnj  38072  cdlemk42  39393  zindbi  41246  jm2.27  41308  nnoeomeqom  41622  rp-brsslt  41675  stoweidlem43  44254  fourierdlem42  44360  ichexmpl1  45631  sepfsepc  46930  iscnrm3rlem8  46950  iscnrm3llem2  46953
  Copyright terms: Public domain W3C validator