Theorem biimtrdi 163

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 144	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 33	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.33bdc  1676  ax11i  1760  equveli  1805  eupickbi  2160  nfabdw  2391  rgen2a  2584  reu6  2993  sseq0  3534  disjel  3547  preq12b  3851  prel12  3852  prneimg  3855  elinti  3935  exmidundif  4294  opthreg  4652  elreldm  4956  issref  5117  relcnvtr  5254  relresfld  5264  funopg  5358  funimass2  5405  f0dom0  5527  fvimacnv  5758  funopdmsn  5829  elunirn  5902  oprabid  6045  op1steq  6337  f1o2ndf1  6388  reldmtpos  6414  rntpos  6418  nntri3or  6656  nnaordex  6691  nnawordex  6692  findcard2  7071  findcard2s  7072  mkvprop  7348  cc2lem  7475  lt2addnq  7614  lt2mulnq  7615  genpelvl  7722  genpelvu  7723  distrlem5prl  7796  distrlem5pru  7797  caucvgprlemnkj  7876  map2psrprg  8015  rereceu  8099  ltxrlt  8235  0mnnnnn0  9424  elnnnn0b  9436  nn0le2is012  9552  btwnz  9589  uz11  9769  nn01to3  9841  zq  9850  xrltso  10021  xltnegi  10060  xnn0lenn0nn0  10090  xnn0xadd0  10092  iccleub  10156  fzdcel  10265  uznfz  10328  2ffzeq  10366  elfzonlteqm1  10445  icogelb  10515  flqeqceilz  10570  modqadd1  10613  modqmul1  10629  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  fzfig  10682  seqf1og  10773  m1expeven  10838  qsqeqor  10902  fundm2domnop0  11099  ccatrcl1  11181  pfxsuff1eqwrdeq  11270  wrdind  11293  wrd2ind  11294  swrdccat3blem  11310  caucvgrelemcau  11531  rexico  11772  fisumss  11943  fsum2dlemstep  11985  ntrivcvgap  12099  fprodssdc  12141  fprod2dlemstep  12173  0dvds  12362  alzdvds  12405  opoe  12446  omoe  12447  opeo  12448  omeo  12449  m1exp1  12452  nn0enne  12453  nn0o1gt2  12456  gcdneg  12543  dfgcd2  12575  algcvgblem  12611  algcvga  12613  eucalglt  12619  coprmdvds  12654  divgcdcoprmex  12664  cncongr1  12665  prm2orodd  12688  prm23lt5  12826  pockthi  12921  f1ocpbl  13384  f1ovscpbl  13385  f1olecpbl  13386  ismnddef  13491  lmodfopnelem1  14328  tg2  14774  tgcl  14778  neii1  14861  neii2  14863  txlm  14993  reopnap  15260  tgioo  15268  addcncntoplem  15275  gausslemma2dlem0i  15776  2lgslem2  15811  2lgs  15823  2lgsoddprmlem3  15830  uhgr0vb  15925  umgredg  15984  uspgrushgr  16019  uspgrupgr  16020  usgruspgr  16022  uhgr2edg  16045  edg0usgr  16086  vtxdg0v  16100  wlkpropg  16121  wlkv  16123  wlkvg  16125  wlkvtxeledgg  16141  wlkl1loop  16155  upgrwlkedg  16158  upgrwlkvtxedg  16161  uspgr2wlkeq  16162  wlkv0  16166  clwwlkccat  16196  clwwlknp  16212  clwwlkext2edg  16217  bj-elssuniab  16323  bj-nn0sucALT  16509  triap  16569