ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anbi12i GIF version

Theorem anbi12i 433
Description: Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
anbi12.1 (𝜑𝜓)
anbi12.2 (𝜒𝜃)
Assertion
Ref Expression
anbi12i ((𝜑𝜒) ↔ (𝜓𝜃))

Proof of Theorem anbi12i
StepHypRef Expression
1 anbi12.1 . . 3 (𝜑𝜓)
21anbi1i 431 . 2 ((𝜑𝜒) ↔ (𝜓𝜒))
3 anbi12.2 . . 3 (𝜒𝜃)
43anbi2i 430 . 2 ((𝜓𝜒) ↔ (𝜓𝜃))
52, 4bitri 173 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  anbi12ci  434  ordir  730  orddi  733  dcan  842  3anbi123i  1093  an6  1216  xorcom  1279  trubifal  1307  truxortru  1310  truxorfal  1311  falxortru  1312  falxorfal  1313  nford  1459  nfand  1460  sbequ8  1727  sbanv  1769  sban  1829  sbbi  1833  sbnf2  1857  eu1  1925  2exeu  1992  2eu4  1993  sbabel  2203  neanior  2292  rexeqbii  2337  r19.26m  2444  reean  2478  reu5  2522  reu2  2729  reu3  2731  eqss  2960  unss  3117  ralunb  3124  ssin  3159  undi  3185  difundi  3189  indifdir  3193  inab  3205  difab  3206  reuss2  3217  reupick  3221  raaan  3327  prss  3520  tpss  3529  prsspw  3536  prneimg  3545  uniin  3600  intun  3646  intpr  3647  brin  3811  brdif  3812  ssext  3957  pweqb  3959  opthg2  3976  copsex4g  3984  opelopabsb  3997  eqopab2b  4016  pwin  4019  pofun  4049  wetrep  4097  ordwe  4300  wessep  4302  reg3exmidlemwe  4303  elxp3  4394  soinxp  4410  relun  4454  inopab  4468  difopab  4469  inxp  4470  opelco2g  4503  cnvco  4520  dmin  4543  intasym  4709  asymref  4710  cnvdif  4730  xpm  4745  xp11m  4759  dfco2  4820  relssdmrn  4841  cnvpom  4860  xpcom  4864  dffun4  4913  dffun4f  4918  funun  4944  funcnveq  4962  fun11  4966  fununi  4967  imadif  4979  imainlem  4980  imain  4981  fnres  5015  fnopabg  5022  fun  5063  fin  5076  dff1o2  5131  brprcneu  5171  fsn  5335  dff1o6  5416  isotr  5456  brabvv  5551  eqoprab2b  5563  dfoprab3  5817  poxp  5853  brtpos2  5866  tfrlem7  5933  dfer2  6107  eqer  6138  iinerm  6178  brecop  6196  eroveu  6197  erovlem  6198  oviec  6212  xpcomco  6300  xpassen  6304  dfmq0qs  6525  dfplq0qs  6526  enq0enq  6527  enq0tr  6530  npsspw  6567  nqprdisj  6640  ltnqpr  6689  ltnqpri  6690  ltexprlemdisj  6702  addcanprg  6712  recexprlemdisj  6726  caucvgprprlemval  6784  addsrpr  6828  mulsrpr  6829  mulgt0sr  6860  addcnsr  6908  mulcnsr  6909  ltresr  6913  addvalex  6918  axcnre  6953  xrnemnf  8697  xrnepnf  8698  elfzuzb  8882  fzass4  8923
  Copyright terms: Public domain W3C validator