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

Theorem 3anbi13d 1548
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 1546 1 (𝜑 → ((𝜓𝜂𝜃) ↔ (𝜒𝜂𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1070
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 383  df-3an 1072
This theorem is referenced by:  3anbi3d  1552  ax12wdemo  2166  f1dom3el3dif  6668  wfrlem1  7565  wfrlem3a  7568  wfrlem15  7581  cofsmo  9292  axdc3lem3  9475  axdc3lem4  9476  iscatd2  16548  psgnunilem1  18119  nn0gsumfz  18586  opprsubrg  19010  lsspropd  19229  mdetunilem3  20637  mdetunilem9  20643  smadiadetr  20699  lmres  21324  cnhaus  21378  regsep2  21400  dishaus  21406  ordthauslem  21407  nconnsubb  21446  pthaus  21661  txhaus  21670  xkohaus  21676  regr1lem  21762  ustval  22225  methaus  22544  metnrmlem3  22883  pmltpclem1  23435  axtgeucl  25591  iscgrad  25923  dfcgra2  25941  f1otrge  25972  axeuclidlem  26062  umgrvad2edg  26326  elwspths2spth  27113  upgr3v3e3cycl  27357  upgr4cycl4dv4e  27362  vdgn1frgrv2  27475  numclwlk1lem1  27555  ex-opab  27625  isnvlem  27799  ajval  28051  adjeu  29082  adjval  29083  adj1  29126  adjeq  29128  cnlnssadj  29273  br8d  29754  lt2addrd  29850  xlt2addrd  29857  measval  30595  br8  31978  br6  31979  br4  31980  frrlem1  32111  brsslt  32231  brcgr3  32484  brsegle  32546  fvray  32579  linedegen  32581  fvline  32582  poimirlem28  33763  isopos  34982  hlsuprexch  35182  2llnjN  35368  2lplnj  35421  cdlemk42  36743  zindbi  38030  jm2.27  38094  stoweidlem43  40771  fourierdlem42  40877
  Copyright terms: Public domain W3C validator