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

Theorem sylan9bb 680
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
Hypotheses
Ref Expression
sylan9bb.1  |-  ( ph  ->  ( ps  <->  ch )
)
sylan9bb.2  |-  ( th 
->  ( ch  <->  ta )
)
Assertion
Ref Expression
sylan9bb  |-  ( (
ph  /\  th )  ->  ( ps  <->  ta )
)

Proof of Theorem sylan9bb
StepHypRef Expression
1 sylan9bb.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21adantr 451 . 2  |-  ( (
ph  /\  th )  ->  ( ps  <->  ch )
)
3 sylan9bb.2 . . 3  |-  ( th 
->  ( ch  <->  ta )
)
43adantl 452 . 2  |-  ( (
ph  /\  th )  ->  ( ch  <->  ta )
)
52, 4bitrd 244 1  |-  ( (
ph  /\  th )  ->  ( ps  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  sylan9bbr  681  bi2anan9  843  baibd  875  rbaibd  876  syl3an9b  1250  sbcom  2029  sbcom2  2053  ax11eq  2132  ax11el  2133  eqeq12  2295  eleq12  2345  sbhypf  2833  ceqsrex2v  2903  sseq12  3201  rexprg  3683  rextpg  3685  breq12  4028  opelopabg  4283  brabg  4284  opelopab2  4285  reusv2lem5  4539  ralxpf  4830  feq23  5378  f00  5426  fconstg  5428  f1oeq23  5466  f1o00  5508  isofrlem  5837  f1oiso  5848  f1oweALT  5851  cbvmpt2x  5924  caovord  6031  caovord3  6033  riota1a  6324  oaordex  6556  oaass  6559  odi  6577  findcard2s  7099  unfilem1  7121  oieu  7254  r1pw  7517  carddomi2  7603  isacn  7671  cdadom2  7813  axdc2  8075  alephval2  8194  fpwwe2cbv  8252  fpwwe2lem2  8254  fpwwecbv  8266  fpwwelem  8267  canthwelem  8272  canthwe  8273  distrlem4pr  8650  axpre-sup  8791  nn0ind-raph  10112  elfz  10788  elfzp12  10861  expeq0  11132  leiso  11397  shftfib  11567  absdvdsb  12547  dvdsabsb  12548  unbenlem  12955  isprs  14064  isdrs  14068  pltval  14094  lubid  14116  istos  14141  isdlat  14296  spwpr2  14337  znfld  16514  tgss2  16725  isopn2  16769  cnpf2  16980  lmbr  16988  isreg2  17105  fclsrest  17719  divstgplem  17803  xmetec  17980  nmogelb  18225  metdstri  18355  tchcph  18667  ulmval  19759  eigrei  22414  eigorthi  22417  jplem1  22848  superpos  22934  chrelati  22944  issiga  23472  eupath2lem1  23901  dfrtrclrec2  24040  br8  24113  br6  24114  br4  24115  brsegle  24731  nndivsub  24896  elo  25041  iepiclem  25823  isfuna  25834  topfne  26290  tailfb  26326  filnetlem1  26327  grpokerinj  26575  rngoisoval  26608  smprngopr  26677  fnelfp  26755  fnelnfp  26757  rexrabdioph  26875  iotasbc2  27620  2llnjN  29756  2lplnj  29809  elpadd0  29998  lauteq  30284  lpolconN  31677
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  df-an 360
  Copyright terms: Public domain W3C validator