Theorem sylan9bb 519

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 486	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒))
3		sylan9bb.2	. . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏))
4	3	adantl 487	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏))
5	2, 4	bitrd 282	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylan9bbr  520  baibd  549  syl3an9b  1463  nanbi12  1533  elequ12  2165  sbcom2  2212  2sb5rf  2504  2sb6rf  2505  eqeqan12d  2777  eleq12  2854  ceqsrex2v  3615  elabd2  3627  elabgt  3629  sseq12  3940  csbie2df  4404  2ralsng  4640  rexprgf  4657  rextpg  4661  breq12  5113  reusv2lem5  5371  opelopabg  5520  brabg  5521  opelopabgf  5522  opelopab2  5523  rbropapd  5544  poeq12d  5571  soeq12d  5589  freq12d  5627  seeq12d  5630  weeq12d  5647  ralxpf  5834  feq23  6720  f00  6794  fconstg  6799  f1oeq23  6845  f1o00  6891  fnelfp  7211  fnelnfp  7213  isofrlem  7379  f1oiso  7390  riota1a  7430  cbvmpox  7544  caovord  7664  caovord3  7666  f1oweALT  8018  mpof1o2d  8174  oaordex  8604  oaass  8607  odi  8625  curf  8928  findcard2s  9219  unfilem1  9335  tfsnfin2  9390  suppeqfsuppbi  9408  oieu  9570  r1pw  9896  carddomi2  10088  isacn  10162  djudom2  10301  axdc2  10566  alephval2  10696  distrlem4pr  11150  axpre-sup  11293  nn0ind-raph  12839  elpq  13143  xnn0xadd0  13417  elfz  13685  elfzp12  13777  expeq0  14275  leiso  14645  wrd2ind  14914  trcleq12lem  15189  dfrtrclrec2  15254  shftfib  15268  absdvdsb  16488  dvdsabsb  16489  dvdsabseq  16527  unbenlem  17130  isprs  18520  isdrs  18525  pltval  18554  lublecllem  18582  istos  18640  isdlat  18746  znfld  21921  tgss2  23360  isopn2  23405  cnpf2  23623  lmbr  23631  isreg2  23750  fclsrest  24398  qustgplem  24495  ustuqtoplem  24613  xmetec  24808  nmogelb  25090  metdstri  25226  tcphcph  25613  ulmval  26764  2lgslem1a  27775  elmade  28300  bdayle  28359  iscgrg  29032  istrlson  30346  ispthson  30385  isspthson  30386  elwwlks2on  30607  acycgrcycl  30810  eupth2lem1  30876  eigrei  32493  eigorthi  32496  jplem1  32927  superpos  33013  chrelati  33023  br8d  33300  ellpi  34032  issiga  34855  eulerpartlemgvv  35119  cplgredgex  36103  br8  36736  br6  36737  br4  36738  brsegle  37088  topfne  37357  tailfb  37380  filnetlem1  37381  nndivsub  37460  bj-rest10  38279  isbasisrelowllem1  38546  isbasisrelowllem2  38547  fvineqsnf1  38601  wl-2sb6d  38758  curunc  38793  poimirlem26  38832  mblfinlem2  38844  cnambfre  38854  itgaddnclem2  38865  ftc1anclem1  38879  grpokerinj  39093  rngoisoval  39177  smprngopr  39252  parteq12  40077  ax12eq  40264  ax12el  40265  2llnjN  40890  2lplnj  40943  elpadd0  41132  lauteq  41418  lpolconN  42810  rexrabdioph  44067  tfsnfin  44615  eliunov2  44940  nzss  45562  iotasbc2  45664  or2expropbilem2  48376  elsetpreimafvbi  48746  reuopreuprim  48881  grlicref  49383  smprngprmrng  49767  cbvmpox2  49779  naryfvalel  50073  line2x  50197  brab2ddw  50271  brab2ddw2  50272