Theorem sylan9bb 509

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)

Hypotheses

Ref	Expression
sylan9bb.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
sylan9bb.2	⊢ (𝜃 → (𝜒 ↔ 𝜏))

Assertion

Ref	Expression
sylan9bb	⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))

Proof of Theorem sylan9bb

Step	Hyp	Ref	Expression
1		sylan9bb.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒))
3		sylan9bb.2	. . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏))
4	3	adantl 481	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏))
5	2, 4	bitrd 279	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  sylan9bbr  510  baibd  539  syl3an9b  1431  nanbi12  1497  sbcom2  2163  2sb5rf  2467  2sb6rf  2468  eqeqan12d  2742  eqeq12OLD  2747  eleq12  2819  sbhypfOLD  3537  ceqsrex2v  3644  elabd2  3658  sseq12  4007  csbie2df  4441  2ralsng  4681  rexprgf  4698  rextpg  4704  breq12  5153  reusv2lem5  5402  opelopabg  5540  brabg  5541  opelopabgf  5542  opelopab2  5543  rbropapd  5566  ralxpf  5849  feq23  6706  f00  6779  fconstg  6784  f1oeq23  6830  f1o00  6874  fnelfp  7184  fnelnfp  7186  isofrlem  7348  f1oiso  7359  riota1a  7399  cbvmpox  7513  caovord  7632  caovord3  7634  f1oweALT  7976  oaordex  8578  oaass  8581  odi  8599  findcard2s  9189  unfilem1  9334  suppeqfsuppbi  9402  oieu  9562  r1pw  9868  carddomi2  9993  isacn  10067  djudom2  10206  axdc2  10472  alephval2  10595  fpwwe2cbv  10653  fpwwe2lem2  10655  fpwwecbv  10667  fpwwelem  10668  canthwelem  10673  canthwe  10674  distrlem4pr  11049  axpre-sup  11192  nn0ind-raph  12692  elpq  12989  xnn0xadd0  13258  elfz  13522  elfzp12  13612  expeq0  14089  leiso  14452  wrd2ind  14705  trcleq12lem  14972  dfrtrclrec2  15037  shftfib  15051  absdvdsb  16251  dvdsabsb  16252  dvdsabseq  16289  unbenlem  16876  isprs  18288  isdrs  18292  pltval  18323  lublecllem  18351  istos  18409  isdlat  18513  znfld  21493  tgss2  22889  isopn2  22935  cnpf2  23153  lmbr  23161  isreg2  23280  fclsrest  23927  qustgplem  24024  ustuqtoplem  24143  xmetec  24339  nmogelb  24632  metdstri  24766  tcphcph  25164  ulmval  26315  2lgslem1a  27323  elmade  27793  iscgrg  28315  istrlson  29520  ispthson  29555  isspthson  29556  elwwlks2on  29769  eupth2lem1  30027  eigrei  31643  eigorthi  31646  jplem1  32077  superpos  32163  chrelati  32173  br8d  32399  issiga  33731  eulerpartlemgvv  33996  cplgredgex  34730  acycgrcycl  34757  br8  35350  br6  35351  br4  35352  brsegle  35704  topfne  35838  tailfb  35861  filnetlem1  35862  nndivsub  35941  bj-elequ12  36155  bj-rest10  36567  isbasisrelowllem1  36834  isbasisrelowllem2  36835  fvineqsnf1  36889  wl-2sb6d  37025  curf  37071  curunc  37075  poimirlem26  37119  mblfinlem2  37131  cnambfre  37141  itgaddnclem2  37152  ftc1anclem1  37166  grpokerinj  37366  rngoisoval  37450  smprngopr  37525  parteq12  38248  ax12eq  38413  ax12el  38414  2llnjN  39040  2lplnj  39093  elpadd0  39282  lauteq  39568  lpolconN  40960  f1o2d2  41724  rexrabdioph  42214  tfsnfin  42781  eliunov2  43109  nzss  43754  iotasbc2  43857  or2expropbilem2  46415  elsetpreimafvbi  46731  reuopreuprim  46866  cbvmpox2  47399  naryfvalel  47703  line2x  47827

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »