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

Theorem sylan9bb 682
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 453 . 2  |-  ( (
ph  /\  th )  ->  ( ps  <->  ch )
)
3 sylan9bb.2 . . 3  |-  ( th 
->  ( ch  <->  ta )
)
43adantl 454 . 2  |-  ( (
ph  /\  th )  ->  ( ch  <->  ta )
)
52, 4bitrd 246 1  |-  ( (
ph  /\  th )  ->  ( ps  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  sylan9bbr  683  bi2anan9  845  baibd  877  rbaibd  878  syl3an9b  1253  nanbi12  1307  sbcomOLD  2167  sbcom2  2192  ax11eq  2272  ax11el  2273  eqeq12  2450  eleq12  2500  sbhypf  3003  ceqsrex2v  3073  sseq12  3373  rexprg  3860  rextpg  3862  breq12  4219  opelopabg  4475  brabg  4476  opelopab2  4477  reusv2lem5  4730  ralxpf  5021  feq23  5581  f00  5630  fconstg  5632  f1oeq23  5670  f1o00  5712  isofrlem  6062  f1oiso  6073  f1oweALT  6076  cbvmpt2x  6152  caovord  6260  caovord3  6262  riota1a  6571  oaordex  6803  oaass  6806  odi  6824  findcard2s  7351  unfilem1  7373  oieu  7510  r1pw  7773  carddomi2  7859  isacn  7927  cdadom2  8069  axdc2  8331  alephval2  8449  fpwwe2cbv  8507  fpwwe2lem2  8509  fpwwecbv  8521  fpwwelem  8522  canthwelem  8527  canthwe  8528  distrlem4pr  8905  axpre-sup  9046  nn0ind-raph  10372  elfz  11051  elfzp12  11128  expeq0  11412  leiso  11710  shftfib  11889  absdvdsb  12870  dvdsabsb  12871  unbenlem  13278  isprs  14389  isdrs  14393  pltval  14419  lubid  14441  istos  14466  isdlat  14621  spwpr2  14662  znfld  16843  tgss2  17054  isopn2  17098  cnpf2  17316  lmbr  17324  isreg2  17443  fclsrest  18058  divstgplem  18152  ustuqtoplem  18271  xmetec  18466  nmogelb  18752  metdstri  18883  tchcph  19196  ulmval  20298  eupath2lem1  21701  eigrei  23339  eigorthi  23342  jplem1  23773  superpos  23859  chrelati  23869  issiga  24496  dfrtrclrec2  25145  br8  25381  br6  25382  br4  25383  brsegle  26044  nndivsub  26209  mblfinlem2  26246  cnambfre  26257  itgaddnclem2  26266  ftc1anclem1  26282  topfne  26372  tailfb  26408  filnetlem1  26409  grpokerinj  26562  rngoisoval  26595  smprngopr  26664  fnelfp  26738  fnelnfp  26740  rexrabdioph  26856  iotasbc2  27599  sbcomwAUX7  29650  sbcom2NEW7  29706  sbcomOLD7  29817  2llnjN  30426  2lplnj  30479  elpadd0  30668  lauteq  30954  lpolconN  32347
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 179  df-an 362
  Copyright terms: Public domain W3C validator