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

This theorem is referenced by:  sylan9bbr  510  baibd  539  syl3an9b  1437  nanbi12  1505  elequ12  2132  sbcom2  2179  2sb5rf  2477  2sb6rf  2478  eqeqan12d  2751  eleq12  2827  ceqsrex2v  3601  elabd2  3613  elabgt  3615  sseq12  3950  csbie2df  4384  2ralsng  4623  rexprgf  4640  rextpg  4644  breq12  5091  reusv2lem5  5339  opelopabg  5486  brabg  5487  opelopabgf  5488  opelopab2  5489  rbropapd  5510  poeq12d  5537  soeq12d  5555  freq12d  5593  seeq12d  5596  weeq12d  5613  ralxpf  5795  feq23  6643  f00  6716  fconstg  6721  f1oeq23  6765  f1o00  6809  fnelfp  7123  fnelnfp  7125  isofrlem  7288  f1oiso  7299  riota1a  7339  cbvmpox  7453  caovord  7571  caovord3  7573  f1oweALT  7918  oaordex  8486  oaass  8489  odi  8507  findcard2s  9093  unfilem1  9208  tfsnfin2  9266  suppeqfsuppbi  9285  oieu  9447  r1pw  9760  carddomi2  9885  isacn  9957  djudom2  10097  axdc2  10362  alephval2  10486  distrlem4pr  10940  axpre-sup  11083  nn0ind-raph  12620  elpq  12916  xnn0xadd0  13190  elfz  13458  elfzp12  13548  expeq0  14045  leiso  14412  wrd2ind  14676  trcleq12lem  14946  dfrtrclrec2  15011  shftfib  15025  absdvdsb  16234  dvdsabsb  16235  dvdsabseq  16273  unbenlem  16870  isprs  18253  isdrs  18258  pltval  18287  lublecllem  18315  istos  18373  isdlat  18479  znfld  21550  tgss2  22962  isopn2  23007  cnpf2  23225  lmbr  23233  isreg2  23352  fclsrest  23999  qustgplem  24096  ustuqtoplem  24214  xmetec  24409  nmogelb  24691  metdstri  24827  tcphcph  25214  ulmval  26358  2lgslem1a  27368  elmade  27863  bdayle  27922  iscgrg  28594  istrlson  29788  ispthson  29825  isspthson  29826  elwwlks2on  30044  eupth2lem1  30303  eigrei  31920  eigorthi  31923  jplem1  32354  superpos  32440  chrelati  32450  br8d  32696  ellpi  33448  issiga  34272  eulerpartlemgvv  34536  cplgredgex  35319  acycgrcycl  35345  br8  35954  br6  35955  br4  35956  brsegle  36306  topfne  36552  tailfb  36575  filnetlem1  36576  nndivsub  36655  bj-rest10  37416  isbasisrelowllem1  37685  isbasisrelowllem2  37686  fvineqsnf1  37740  wl-2sb6d  37897  curf  37933  curunc  37937  poimirlem26  37981  mblfinlem2  37993  cnambfre  38003  itgaddnclem2  38014  ftc1anclem1  38028  grpokerinj  38228  rngoisoval  38312  smprngopr  38387  parteq12  39214  ax12eq  39401  ax12el  39402  2llnjN  40027  2lplnj  40080  elpadd0  40269  lauteq  40555  lpolconN  41947  f1o2d2  42688  rexrabdioph  43240  tfsnfin  43798  eliunov2  44124  nzss  44762  iotasbc2  44865  or2expropbilem2  47493  elsetpreimafvbi  47863  reuopreuprim  47998  grlicref  48500  cbvmpox2  48824  naryfvalel  49118  line2x  49242  brab2ddw  49316  brab2ddw2  49317