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

Theorem 3anbi3i 1156
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 260 . 2 (𝜒𝜒)
2 biid 260 . 2 (𝜃𝜃)
3 3anbi1i.1 . 2 (𝜑𝜓)
41, 2, 33anbi123i 1152 1 ((𝜒𝜃𝜑) ↔ (𝜒𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  w3a 1084
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 395  df-3an 1086
This theorem is referenced by:  cadcomb  1607  dfwrecsOLD  8328  dfer2  8735  ttrclresv  9760  axgroth2  10868  oppgsubm  19359  xrsdsreclb  21410  ordthaus  23379  qtopeu  23711  regr1lem2  23735  isfbas2  23830  isclmp  25115  umgr2edg1  29147  xrge0adddir  32901  isros  34001  bnj964  34788  bnj1033  34814  cusgr3cyclex  34964  dfon2lem7  35613  outsideofcom  35952  linecom  35974  linerflx2  35975  topdifinffinlem  37054  rdgeqoa  37077  ishlat2  39051  lhpex2leN  39712  aks6d1c1rh  41823  sn-isghm  42327  lmbr3v  45366  lmbr3  45368  fourierdlem103  45830  fourierdlem104  45831  issmf  46349  issmff  46355  issmfle  46366  issmfgt  46377  issmfge  46391  funcf2lem  48339
  Copyright terms: Public domain W3C validator