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

Theorem anbi12i 441
Description: Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
anbi12.1  |-  ( ph  <->  ps )
anbi12.2  |-  ( ch  <->  th )
Assertion
Ref Expression
anbi12i  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)

Proof of Theorem anbi12i
StepHypRef Expression
1 anbi12.1 . . 3  |-  ( ph  <->  ps )
21anbi1i 439 . 2  |-  ( (
ph  /\  ch )  <->  ( ps  /\  ch )
)
3 anbi12.2 . . 3  |-  ( ch  <->  th )
43anbi2i 438 . 2  |-  ( ( ps  /\  ch )  <->  ( ps  /\  th )
)
52, 4bitri 177 1  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)
Colors of variables: wff set class
Syntax hints:    /\ wa 101    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  anbi12ci  442  ordir  741  orddi  744  dcan  853  3anbi123i  1104  an6  1227  xorcom  1295  trubifal  1323  truxortru  1326  truxorfal  1327  falxortru  1328  falxorfal  1329  nford  1475  nfand  1476  sbequ8  1743  sbanv  1785  sban  1845  sbbi  1849  sbnf2  1873  eu1  1941  2exeu  2008  2eu4  2009  sbabel  2219  neanior  2307  rexeqbii  2354  r19.26m  2461  reean  2495  reu5  2539  reu2  2751  reu3  2753  eqss  2987  unss  3144  ralunb  3151  ssin  3186  undi  3212  difundi  3216  indifdir  3220  inab  3232  difab  3233  reuss2  3244  reupick  3248  raaan  3354  prss  3547  tpss  3556  prsspw  3563  prneimg  3572  uniin  3627  intun  3673  intpr  3674  brin  3838  brdif  3839  ssext  3984  pweqb  3986  opthg2  4003  copsex4g  4011  opelopabsb  4024  eqopab2b  4043  pwin  4046  pofun  4076  wetrep  4124  ordwe  4327  wessep  4329  reg3exmidlemwe  4330  elxp3  4421  soinxp  4437  relun  4481  inopab  4495  difopab  4496  inxp  4497  opelco2g  4530  cnvco  4547  dmin  4570  intasym  4736  asymref  4737  cnvdif  4757  xpm  4772  xp11m  4786  dfco2  4847  relssdmrn  4868  cnvpom  4887  xpcom  4891  dffun4  4940  dffun4f  4945  funun  4971  funcnveq  4989  fun11  4993  fununi  4994  imadif  5006  imainlem  5007  imain  5008  fnres  5042  fnopabg  5049  fun  5090  fin  5103  dff1o2  5158  brprcneu  5198  fsn  5362  dff1o6  5443  isotr  5483  brabvv  5578  eqoprab2b  5590  dfoprab3  5844  poxp  5880  cnvoprab  5882  f1od2  5883  brtpos2  5896  tfrlem7  5963  dfer2  6137  eqer  6168  iinerm  6208  brecop  6226  eroveu  6227  erovlem  6228  oviec  6242  xpcomco  6330  xpassen  6334  dfmq0qs  6584  dfplq0qs  6585  enq0enq  6586  enq0tr  6589  npsspw  6626  nqprdisj  6699  ltnqpr  6748  ltnqpri  6749  ltexprlemdisj  6761  addcanprg  6771  recexprlemdisj  6785  caucvgprprlemval  6843  addsrpr  6887  mulsrpr  6888  mulgt0sr  6919  addcnsr  6967  mulcnsr  6968  ltresr  6972  addvalex  6977  axcnre  7012  xrnemnf  8799  xrnepnf  8800  elfzuzb  8985  fzass4  9026
  Copyright terms: Public domain W3C validator