MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitri Unicode version

Theorem 3bitri 262
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3bitri.1  |-  ( ph  <->  ps )
3bitri.2  |-  ( ps  <->  ch )
3bitri.3  |-  ( ch  <->  th )
Assertion
Ref Expression
3bitri  |-  ( ph  <->  th )

Proof of Theorem 3bitri
StepHypRef Expression
1 3bitri.1 . 2  |-  ( ph  <->  ps )
2 3bitri.2 . . 3  |-  ( ps  <->  ch )
3 3bitri.3 . . 3  |-  ( ch  <->  th )
42, 3bitri 240 . 2  |-  ( ps  <->  th )
51, 4bitri 240 1  |-  ( ph  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  bibi1i  305  orbi1i  506  orass  510  or32  513  pm5.32  617  an32  773  excxor  1309  trunanfal  1355  falxortru  1360  nic-axALT  1439  tbw-bijust  1463  rb-bijust  1514  19.43  1605  19.43OLD  1606  excom13  1743  nf4  1873  19.12vv  1903  3exdistr  1915  4exdistr  1916  eeeanv  1919  ee4anv  1920  sb3an  2075  sbnf2  2113  sb8eu  2227  2eu4  2292  2eu7  2295  2eu8  2296  r19.26-3  2753  rexcom13  2778  cbvreu  2838  ceqsex2  2900  ceqsex4v  2903  ralrab2  3007  rexrab2  3009  reu2  3029  rmo4  3034  reu8  3037  2reu5lem3  3048  rmo2  3152  rmo3  3154  dfss2  3245  ss2rab  3325  rabss  3326  ssrab  3327  dfss4  3479  undi  3492  undif3  3505  difin2  3506  dfnul2  3533  disj  3571  disj4  3579  elimif  3670  disjsn  3769  ssunpr  3855  sspr  3856  sstp  3857  uni0b  3931  uni0c  3932  ssint  3957  iunss  4022  iundif2  4048  disjor  4086  nfnid  4283  ssextss  4306  eqvinop  4330  opcom  4339  opeqsn  4341  opeqpr  4342  brabsbOLD  4353  brabsb  4355  opelopabf  4368  dfid3  4389  pofun  4409  sotrieq  4420  trsuc2OLD  4556  uniuni  4606  reusv2lem4  4617  dflim3  4717  dfom2  4737  opeliunxp  4819  xpiundi  4822  brinxp2  4830  ssrel  4855  reliun  4885  cnvuni  4945  dmopab3  4970  opelres  5039  elres  5069  elsnres  5070  asymref2  5139  intirr  5140  xpeq0  5179  ssrnres  5195  dminxp  5197  dfrel4v  5204  dmsnn0  5217  elxp4  5239  elxp5  5240  rnco  5258  sb8iota  5305  dffun2  5344  fun11  5394  isarep1  5410  dff1o4  5560  fnressn  5786  opabex3d  5852  opabex3  5853  dff1o6  5875  fliftel  5892  oprabid  5966  mpt22eqb  6037  ralrnmpt2  6042  exopxfr  6267  xporderlem  6310  fvopab5  6373  opabiota  6377  tz7.48lem  6537  seqomlem2  6547  oaord  6629  nnaord  6701  ecid  6808  mptelixpg  6938  elixpsn  6940  mapsnen  7023  xpsnen  7031  xpcomco  7037  xpassen  7041  omxpenlem  7048  dom0  7074  modom  7148  dfsup2OLD  7283  tz9.12lem3  7548  rankxpsuc  7639  cp  7648  cardprclem  7699  infxpenlem  7728  dfac5lem1  7837  dfac5lem2  7838  dfac5lem5  7841  dfac10c  7851  kmlem3  7865  kmlem12  7874  kmlem13  7875  kmlem14  7876  kmlem15  7877  ackbij2  7956  cflim2  7976  dffin7-2  8111  dfacfin7  8112  fin1a2lem12  8124  axdc3lem3  8165  cfpwsdom  8293  recmulnq  8675  genpass  8720  psslinpr  8742  suplem2pr  8764  opelreal  8839  ltxrlt  8980  addid1  9079  fimaxre  9788  elnn0  10056  elnn0z  10125  nnwos  10375  elxr  10547  xrnepnf  10550  elfzuzb  10881  elfzo2  10967  sqeqori  11305  fsumcom2  12328  rpnnen2  12595  gcdcllem1  12781  isprm2  12857  pythagtriplem2  12961  infpn2  13051  4sqlem12  13094  eldmcoa  13990  oduposb  14333  isnsg2  14740  isnsg4  14753  efgcpbllemb  15157  dmdprd  15329  dprdval  15331  dprdw  15338  dprd2d2  15372  dfrhm2  15591  issubrg  15638  islmim  15908  lbsextlem2  16005  opsrtoslem1  16318  pjfval2  16709  istps3OLD  16760  ntreq0  16914  cmpsub  17227  2ndcdisj  17282  txbas  17362  elpt  17367  txkgen  17446  xkococn  17454  fbun  17631  trfil2  17678  fin1aufil  17723  alexsubALTlem3  17839  divstgplem  17899  eltsms  17911  metrest  18166  srabn  18875  ellogdm  20091  1cubr  20243  leibpilem2  20342  dmarea  20357  vmasum  20561  dchrelbas2  20582  h2hcau  21667  h2hlm  21668  axhcompl-zf  21686  shlesb1i  22073  shne0i  22135  chnlei  22172  cmbr2i  22283  pjneli  22410  ho02i  22517  adjsym  22521  adjeu  22577  lnopeqi  22696  largei  22955  atoml2i  23071  cdj3lem3b  23128  or3di  23138  mo5f  23161  rmo3f  23171  rmo4fOLD  23172  disjorf  23217  1stpreima  23296  2ndpreima  23297  xrdifh  23342  eliccioo  23382  cnextcn  23504  ustn0  23524  fmucndlem  23585  restmetu  23615  ind1a  23684  elunirnmbfm  23867  ballotlemodife  24004  cvmlift2lem1  24237  3orit  24470  brtp  24664  dftr6  24665  dfpo2  24670  eldm3  24677  elrn3  24678  19.12b  24716  sspred  24732  predreseq  24737  preduz  24758  wfi  24765  frind  24801  nofulllem5  24918  brtxp  24978  brtxp2  24979  brpprod  24983  brpprod3a  24984  ellimits  25008  elfuns  25012  elsingles  25015  brimg  25034  brapply  25035  brcup  25036  brcap  25037  brsuccf  25038  funpartlem  25039  brrestrict  25046  dfrdg4  25047  tfrqfree  25048  altopthc  25064  altopthd  25065  axlowdimlem13  25141  axeuclidlem  25149  fvtransport  25214  hfext  25372  df3nandALT2  25395  areacirclem6  25522  cnvresimaOLD  25550  filnetlem4  25654  isbnd2  25830  prtlem70  26038  prtlem16  26060  raldifsni  26076  coeq0  26154  fz1eqin  26171  7rexfrabdioph  26204  rmydioph  26430  dford4  26445  pm13.196a  26937  compneOLD  26966  2reu7  27292  2reu8  27293  dfdfat2  27319  aovov0bi  27384  4fvwrd4  27491  trls  27671  4cycl4v4e  27773  4cycl4dv4e  27775  frgra3v  27818  eelT11  28217  eelTT1  28223  eelT01  28224  eel0T1  28225  uunTT1  28311  uunTT1p1  28312  uunTT1p2  28313  uunT11  28314  uunT11p1  28315  uunT11p2  28316  uun111  28323  bnj250  28471  bnj334  28483  bnj345  28484  bnj89  28492  bnj115  28496  bnj919  28542  bnj1304  28597  bnj92  28639  bnj124  28648  bnj126  28650  bnj154  28655  bnj155  28656  bnj523  28664  bnj526  28665  bnj540  28669  bnj581  28685  bnj916  28710  bnj929  28713  bnj964  28720  bnj978  28726  bnj983  28728  bnj1039  28746  bnj1040  28747  bnj1123  28761  bnj1128  28765  bnj1398  28809  sbnf2NEW7  29009  sb3anNEW7  29041  excom13OLD7  29079  19.12vvOLD7  29085  eeeanvOLD7  29088  ee4anvOLD7  29089  ishlat2  29595  polval2N  30147  dicelval3  31422  mapdordlem1a  31876
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator