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  2042  sbcom2  2066  ax11eq  2145  ax11el  2146  eqeq12  2308  eleq12  2358  sbhypf  2846  ceqsrex2v  2916  sseq12  3214  rexprg  3696  rextpg  3698  breq12  4044  opelopabg  4299  brabg  4300  opelopab2  4301  reusv2lem5  4555  ralxpf  4846  feq23  5394  f00  5442  fconstg  5444  f1oeq23  5482  f1o00  5524  isofrlem  5853  f1oiso  5864  f1oweALT  5867  cbvmpt2x  5940  caovord  6047  caovord3  6049  riota1a  6340  oaordex  6572  oaass  6575  odi  6593  findcard2s  7115  unfilem1  7137  oieu  7270  r1pw  7533  carddomi2  7619  isacn  7687  cdadom2  7829  axdc2  8091  alephval2  8210  fpwwe2cbv  8268  fpwwe2lem2  8270  fpwwecbv  8282  fpwwelem  8283  canthwelem  8288  canthwe  8289  distrlem4pr  8666  axpre-sup  8807  nn0ind-raph  10128  elfz  10804  elfzp12  10877  expeq0  11148  leiso  11413  shftfib  11583  absdvdsb  12563  dvdsabsb  12564  unbenlem  12971  isprs  14080  isdrs  14084  pltval  14110  lubid  14132  istos  14157  isdlat  14312  spwpr2  14353  znfld  16530  tgss2  16741  isopn2  16785  cnpf2  16996  lmbr  17004  isreg2  17121  fclsrest  17735  divstgplem  17819  xmetec  17996  nmogelb  18241  metdstri  18371  tchcph  18683  ulmval  19775  eigrei  22430  eigorthi  22433  jplem1  22864  superpos  22950  chrelati  22960  issiga  23487  eupath2lem1  23916  dfrtrclrec2  24055  br8  24184  br6  24185  br4  24186  brsegle  24803  nndivsub  24968  elo  25144  iepiclem  25926  isfuna  25937  topfne  26393  tailfb  26429  filnetlem1  26430  grpokerinj  26678  rngoisoval  26711  smprngopr  26780  fnelfp  26858  fnelnfp  26860  rexrabdioph  26978  iotasbc2  27723  sbcomwAUX7  29562  sbcomOLD7  29709  sbcom2OLD7  29715  2llnjN  30378  2lplnj  30431  elpadd0  30620  lauteq  30906  lpolconN  32299
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