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

Theorem 3bitr3i 290
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.)
Hypotheses
Ref Expression
3bitr3i.1 (𝜑𝜓)
3bitr3i.2 (𝜑𝜒)
3bitr3i.3 (𝜓𝜃)
Assertion
Ref Expression
3bitr3i (𝜒𝜃)

Proof of Theorem 3bitr3i
StepHypRef Expression
1 3bitr3i.2 . . 3 (𝜑𝜒)
2 3bitr3i.1 . . 3 (𝜑𝜓)
31, 2bitr3i 266 . 2 (𝜒𝜓)
4 3bitr3i.3 . 2 (𝜓𝜃)
53, 4bitri 264 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 196
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 197
This theorem is referenced by:  an12  873  xorass  1617  cbval2  2424  cbvaldva  2426  sbco2d  2553  sbcom  2555  equsb3  2569  equsb3ALT  2570  elsb3  2571  elsb4  2572  sb7f  2590  sbco4lem  2602  eq2tri  2821  eqsb3  2866  clelsb3  2867  clelsb3f  2906  r19.35  3222  ralcom4  3364  rexcom4  3365  ceqsralt  3369  gencbvex  3390  gencbval  3392  ceqsrexbv  3476  euind  3534  reuind  3552  sbccomlem  3649  sbccom  3650  csbcom  4137  difcom  4197  eqsn  4506  uniintsn  4666  disjxun  4802  reusv2lem4  5021  exss  5080  opab0  5157  elxp2OLD  5290  eqbrriv  5372  dm0rn0  5497  dfres2  5611  qfto  5675  rninxp  5731  coeq0  5805  fununi  6125  dffv2  6433  fndmin  6487  fnprb  6636  fntpb  6637  dfoprab2  6866  dfer2  7912  eceqoveq  8019  euen1  8191  xpsnen  8209  xpassen  8219  marypha2lem3  8508  rankuni  8899  card1  8984  alephislim  9096  dfacacn  9155  kmlem4  9167  ac6num  9493  zorn2lem4  9513  fpwwe2lem8  9651  fpwwe2lem12  9655  mappsrpr  10121  sqeqori  13170  trclublem  13935  fprodle  14926  vdwmc2  15885  txflf  22011  metustid  22560  caucfil  23281  ovolgelb  23448  dfcgra2  25920  axcontlem5  26047  frgr3v  27429  nmoubi  27936  hvsubaddi  28232  hlimeui  28406  omlsilem  28570  pjoml3i  28754  hodsi  28943  nmopub  29076  nmfnleub  29093  nmopcoadj0i  29271  pjin3i  29362  or3dir  29617  ralcom4f  29625  rexcom4f  29626  uniinn0  29673  ordtconnlem1  30279  bnj62  31095  bnj610  31124  bnj1143  31168  bnj1533  31229  bnj543  31270  bnj545  31272  bnj594  31289  ceqsralv2  31914  brsuccf  32354  brfullfun  32361  filnetlem4  32682  bj-ssbcom3lem  32956  bj-cbval2v  33043  bj-clelsb3  33154  icorempt2  33510  poimirlem13  33735  poimirlem14  33736  poimirlem21  33743  poimirlem22  33744  poimir  33755  sbccom2lem  34242  eldmqsres  34375  opelinxp  34434  alrmomorn  34446  xrninxp2  34474  isltrn2N  35909  moxfr  37757  ifporcor  38308  ifpancor  38310  ifpbicor  38322  ifpnorcor  38327  ifpnancor  38328  ifpororb  38352  relexp0eq  38495  hashnzfzclim  39023  pm11.6  39094  sbc3or  39240  cbvexsv  39264  sprvalpwn0  42243  copisnmnd  42319
  Copyright terms: Public domain W3C validator