Theorem biimtrdi 252

Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)

Hypotheses

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

Assertion

Ref	Expression
biimtrdi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem biimtrdi

Step	Hyp	Ref	Expression
1		biimtrdi.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 228	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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

This theorem is referenced by:  ax12i  1969  sb4a  2478  hbsb2  2480  dfsb2  2491  2eu2  2647  nfabdwOLD  2926  reu6  3722  2reu2  3892  sseq0  4399  disjel  4456  disjpss  4460  preq12b  4851  prneimg  4855  preqsnd  4859  elinti  4959  zfrepclf  5294  dtruALT2  5368  dtruOLD  5441  opth1g  5478  sbcop1  5488  snopeqop  5506  propeqop  5507  otsndisj  5519  otiunsndisj  5520  iunopeqop  5521  po2ne  5604  soasym  5619  elreldm  5934  dfres3  5986  relcnvtrg  6265  relresfld  6275  elpredimg  6315  ordtr2  6408  ordssun  6466  funopg  6582  funimass2  6631  f0dom0  6775  elfv2ex  6937  fveqdmss  7080  eldmrexrnb  7093  fvcofneq  7094  funopsn  7148  funopdmsn  7150  funsndifnop  7151  elunirn  7253  2f1fvneq  7262  oprabidw  7443  oprabid  7444  brfvopab  7469  limuni3  7845  peano5  7888  peano5OLD  7889  op1steq  8023  el2mpocsbcl  8076  bropopvvv  8081  bropfvvvv  8083  f1o2ndf1  8113  frxp  8117  fnwelem  8122  poxp2  8134  suppimacnv  8164  fvn0elsuppb  8171  suppfnss  8179  reldmtpos  8225  rntpos  8230  seqomlem2  8457  oaordi  8552  oa00  8565  oalimcl  8566  omeulem1  8588  nnaordi  8624  ecopovtrn  8820  undifixp  8934  mapdom2  9154  unxpdomlem3  9258  en1eqsn  9280  enp1iOLD  9286  findcard2OLD  9290  infssuni  9349  wdompwdom  9579  preleqg  9616  opthreg  9619  inf3lemd  9628  inf3lem2  9630  inf3lem6  9634  cnfcomlem  9700  cnfcom3  9705  karden  9896  carden2a  9967  alephdom  10082  dfac5lem4  10127  dfac12r  10147  kmlem2  10152  kmlem12  10162  cfslb2n  10269  alephsing  10277  fin23lem30  10343  fin1a2lem6  10406  fin1a2lem13  10413  axcc2lem  10437  domtriomlem  10443  axdc3lem2  10452  axdc4lem  10456  brdom6disj  10533  alephexp1  10580  pwfseq  10665  addnidpi  10902  indpi  10908  nqereu  10930  ltsonq  10970  distrlem5pr  11028  addcanpr  11047  suplem1pr  11053  suplem2pr  11054  ltsrpr  11078  ltsosr  11095  sqgt0sr  11107  leltne  11310  ltnsym  11319  ltlen  11322  eqlei  11331  eqlei2  11332  infm3  12180  nnunb  12475  0mnnnnn0  12511  elnnnn0b  12523  nn0ge2m1nn  12548  nn0le2is012  12633  btwnz  12672  uz11  12854  xrleltne  13131  xltnegi  13202  xnn0lenn0nn0  13231  xnn0xadd0  13233  xmulasslem2  13268  reltxrnmnf  13328  icogelb  13382  iccleub  13386  uznfz  13591  2ffzeq  13629  elfzonlteqm1  13715  elfzo0l  13729  elfznelfzob  13745  elfzr  13752  elfzlmr  13753  injresinjlem  13759  injresinj  13760  fleqceilz  13826  modadd1  13880  modmul1  13896  modirr  13914  addmodlteq  13918  uzrdgfni  13930  fsuppmapnn0fiub0  13965  fsuppmapnn0ub  13967  seqf1o  14016  expnngt1  14211  hashrabsn01  14340  hashrabsn1  14341