Theorem sylan9bb 699

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

Step	Hyp	Ref	Expression
1		sylan9bb.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	adantr 465	. 2 |- ( ( ph /\ th ) -> ( ps <-> ch ) )
3		sylan9bb.2	. . 3 |- ( th -> ( ch <-> ta ) )
4	3	adantl 466	. 2 |- ( ( ph /\ th ) -> ( ch <-> ta ) )
5	2, 4	bitrd 253	1 |- ( ( ph /\ th ) -> ( ps <-> ta ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  sylan9bbr  700  bi2anan9  868  baibd  900  rbaibd  901  syl3an9b  1287  nanbi12  1343  sbcom2  2151  sbcom2OLD  2152  2sb5rf  2159  2sb6rf  2160  ax12eq  2242  ax12el  2243  eqeq12  2455  eleq12  2505  sbhypf  3022  ceqsrex2v  3098  sseq12  3382  rexprg  3929  rextpg  3931  breq12  4300  reusv2lem5  4500  opelopabg  4610  brabg  4611  opelopab2  4612  ralxpf  4989  feq23  5548  f00  5596  fconstg  5600  f1oeq23  5638  f1o00  5676  fnelfp  5909  fnelnfp  5911  isofrlem  6034  f1oiso  6045  riota1a  6075  cbvmpt2x  6167  caovord  6277  caovord3  6279  f1oweALT  6564  oaordex  7000  oaass  7003  odi  7021  findcard2s  7556  unfilem1  7579  suppeqfsuppbi  7637  oieu  7756  r1pw  8055  carddomi2  8143  isacn  8217  cdadom2  8359  axdc2  8621  alephval2  8739  fpwwe2cbv  8800  fpwwe2lem2  8802  fpwwecbv  8814  fpwwelem  8815  canthwelem  8820  canthwe  8821  distrlem4pr  9198  axpre-sup  9339  nn0ind-raph  10745  elfz  11446  elfzp12  11542  expeq0  11897  leiso  12215  wrd2ind  12375  shftfib  12564  absdvdsb  13554  dvdsabsb  13555  unbenlem  13972  isprs  15103  isdrs  15107  pltval  15133  lublecllem  15161  istos  15208  isdlat  15366  znfld  17996  tgss2  18595  isopn2  18639  cnpf2  18857  lmbr  18865  isreg2  18984  fclsrest  19600  divstgplem  19694  ustuqtoplem  19817  xmetec  20012  nmogelb  20298  metdstri  20430  tchcph  20755  ulmval  21848  iscgrg  22968  eupath2lem1  23601  eigrei  25241  eigorthi  25244  jplem1  25675  superpos  25761  chrelati  25771  br8d  25945  issiga  26557  eulerpartlemgvv  26762  dfrtrclrec2  27348  br8  27569  br6  27570  br4  27571  brsegle  28142  nndivsub  28306  wl-2sb6d  28387  mblfinlem2  28432  cnambfre  28443  itgaddnclem2  28454  ftc1anclem1  28470  topfne  28565  tailfb  28601  filnetlem1  28602  grpokerinj  28753  rngoisoval  28786  smprngopr  28855  rexrabdioph  29135  iotasbc2  29677  cbvmpt2x2  30729  bj-elequ12  32178  2llnjN  33214  2lplnj  33267  elpadd0  33456  lauteq  33742  lpolconN  35135