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

Theorem 3anbi3i 1159
Description: Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
Hypothesis
Ref Expression
3anbi1i.1 (𝜑𝜓)
Assertion
Ref Expression
3anbi3i ((𝜒𝜃𝜑) ↔ (𝜒𝜃𝜓))

Proof of Theorem 3anbi3i
StepHypRef Expression
1 biid 261 . 2 (𝜒𝜒)
2 biid 261 . 2 (𝜃𝜃)
3 3anbi1i.1 . 2 (𝜑𝜓)
41, 2, 33anbi123i 1155 1 ((𝜒𝜃𝜑) ↔ (𝜒𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  w3a 1086
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 207  df-an 396  df-3an 1088
This theorem is referenced by:  cadcomb  1612  dfwrecsOLD  8339  dfer2  8747  ttrclresv  9758  axgroth2  10866  oppgsubm  19382  xrsdsreclb  21432  ordthaus  23393  qtopeu  23725  regr1lem2  23749  isfbas2  23844  isclmp  25131  umgr2edg1  29229  xrge0adddir  33024  isros  34170  bnj964  34958  bnj1033  34984  cusgr3cyclex  35142  dfon2lem7  35791  outsideofcom  36130  linecom  36152  linerflx2  36153  topdifinffinlem  37349  rdgeqoa  37372  ishlat2  39355  lhpex2leN  40016  aks6d1c1rh  42127  sn-isghm  42688  lmbr3v  45765  lmbr3  45767  fourierdlem103  46229  fourierdlem104  46230  issmf  46748  issmff  46754  issmfle  46765  issmfgt  46776  issmfge  46790  grtriproplem  47911  grtrif1o  47914  funcf2lem  48930
  Copyright terms: Public domain W3C validator