Theorem sylan9bb 458

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 274	. 2 |- ( ( ph /\ th ) -> ( ps <-> ch ) )
3		sylan9bb.2	. . 3 |- ( th -> ( ch <-> ta ) )
4	3	adantl 275	. 2 |- ( ( ph /\ th ) -> ( ch <-> ta ) )
5	2, 4	bitrd 187	1 |- ( ( ph /\ th ) -> ( ps <-> ta ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylan9bbr  459  bi2anan9  596  baibd  913  rbaibd  914  syl3an9b  1300  sbcomxyyz  1960  eqeq12  2178  eleq12  2231  sbhypf  2775  ceqsrex2v  2858  sseq12  3167  rexprg  3628  rextpg  3630  breq12  3987  opelopabg  4246  brabg  4247  opelopab2  4248  ralxpf  4750  rexxpf  4751  feq23  5323  f00  5379  fconstg  5384  f1oeq23  5424  f1o00  5467  f1oiso  5794  riota1a  5817  cbvmpox  5920  caovord  6013  caovord3  6015  rbropapd  6210  genpelvl  7453  genpelvu  7454  nn0ind-raph  9308  elpq  9586  xnn0xadd0  9803  elfz  9950  elfzp12  10034  shftfibg  10762  shftfib  10765  absdvdsb  11749  dvdsabsb  11750  dvdsabseq  11785  tgss2  12719  lmbr  12853  xmetec  13077