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

Theorem anbi12i 448
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 446 . 2 ((𝜑𝜒) ↔ (𝜓𝜒))
3 anbi12.2 . . 3 (𝜒𝜃)
43anbi2i 445 . 2 ((𝜓𝜒) ↔ (𝜓𝜃))
52, 4bitri 182 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  anbi12ci  449  ordir  764  orddi  767  dcan  876  3anbi123i  1128  an6  1253  xorcom  1320  trubifal  1348  truxortru  1351  truxorfal  1352  falxortru  1353  falxorfal  1354  nford  1500  nfand  1501  sbequ8  1769  sbanv  1811  sban  1871  sbbi  1875  sbnf2  1899  eu1  1967  2exeu  2034  2eu4  2035  sbabel  2245  neanior  2333  rexeqbii  2380  r19.26m  2489  reean  2523  reu5  2567  reu2  2781  reu3  2783  eqss  3015  unss  3147  ralunb  3154  ssin  3195  undi  3219  difundi  3223  indifdir  3227  inab  3239  difab  3240  reuss2  3251  reupick  3255  raaan  3355  prss  3549  tpss  3558  prsspw  3565  prneimg  3574  uniin  3629  intun  3675  intpr  3676  brin  3840  brdif  3841  ssext  3984  pweqb  3986  opthg2  4002  copsex4g  4010  opelopabsb  4023  eqopab2b  4042  pwin  4045  pofun  4075  wetrep  4123  ordwe  4326  wessep  4328  reg3exmidlemwe  4329  elxp3  4420  soinxp  4436  relun  4482  inopab  4496  difopab  4497  inxp  4498  opelco2g  4531  cnvco  4548  dmin  4571  intasym  4739  asymref  4740  cnvdif  4760  xpm  4775  xp11m  4789  dfco2  4850  relssdmrn  4871  cnvpom  4890  xpcom  4894  dffun4  4943  dffun4f  4948  funun  4974  funcnveq  4993  fun11  4997  fununi  4998  imadif  5010  imainlem  5011  imain  5012  fnres  5046  fnopabg  5053  fun  5094  fin  5107  dff1o2  5162  brprcneu  5202  fsn  5367  dff1o6  5447  isotr  5487  brabvv  5582  eqoprab2b  5594  dfoprab3  5848  poxp  5884  cnvoprab  5886  f1od2  5887  brtpos2  5900  tfrlem7  5966  dfer2  6173  eqer  6204  iinerm  6244  brecop  6262  eroveu  6263  erovlem  6264  oviec  6278  xpcomco  6370  xpassen  6374  infmoti  6500  dfmq0qs  6681  dfplq0qs  6682  enq0enq  6683  enq0tr  6686  npsspw  6723  nqprdisj  6796  ltnqpr  6845  ltnqpri  6846  ltexprlemdisj  6858  addcanprg  6868  recexprlemdisj  6882  caucvgprprlemval  6940  addsrpr  6984  mulsrpr  6985  mulgt0sr  7016  addcnsr  7064  mulcnsr  7065  ltresr  7069  addvalex  7074  axcnre  7109  supinfneg  8764  infsupneg  8765  xrnemnf  8929  xrnepnf  8930  elfzuzb  9115  fzass4  9156  rexanre  10244  infssuzex  10489  isprm3  10644
  Copyright terms: Public domain W3C validator