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

Theorem 3anbi3i 1153
 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 263 . 2 (𝜒𝜒)
2 biid 263 . 2 (𝜃𝜃)
3 3anbi1i.1 . 2 (𝜑𝜓)
41, 2, 33anbi123i 1149 1 ((𝜒𝜃𝜑) ↔ (𝜒𝜃𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208   ∧ w3a 1081 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 209  df-an 399  df-3an 1083 This theorem is referenced by:  cadcomb  1607  dfer2  8282  axgroth2  10239  oppgsubm  18482  xrsdsreclb  20584  ordthaus  21984  qtopeu  22316  regr1lem2  22340  isfbas2  22435  isclmp  23693  umgr2edg1  26985  xrge0adddir  30672  isros  31420  bnj964  32208  bnj1033  32234  cusgr3cyclex  32376  dfon2lem7  33027  outsideofcom  33582  linecom  33604  linerflx2  33605  topdifinffinlem  34620  rdgeqoa  34643  ishlat2  36481  lhpex2leN  37141  lmbr3v  42015  lmbr3  42017  fourierdlem103  42484  fourierdlem104  42485  issmf  42995  issmff  43001  issmfle  43012  issmfgt  43023  issmfge  43036
 Copyright terms: Public domain W3C validator