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  1678  ax11i  1762  equveli  1807  eupickbi  2162  nfabdw  2393  rgen2a  2586  reu6  2995  sseq0  3536  disjel  3549  preq12b  3853  prel12  3854  prneimg  3857  elinti  3937  exmidundif  4296  opthreg  4654  elreldm  4958  issref  5119  relcnvtr  5256  relresfld  5266  funopg  5360  funimass2  5408  f0dom0  5530  fvimacnv  5762  funopdmsn  5834  elunirn  5907  oprabid  6050  op1steq  6342  f1o2ndf1  6393  reldmtpos  6419  rntpos  6423  nntri3or  6661  nnaordex  6696  nnawordex  6697  findcard2  7078  findcard2s  7079  mkvprop  7357  cc2lem  7485  lt2addnq  7624  lt2mulnq  7625  genpelvl  7732  genpelvu  7733  distrlem5prl  7806  distrlem5pru  7807  caucvgprlemnkj  7886  map2psrprg  8025  rereceu  8109  ltxrlt  8245  0mnnnnn0  9434  elnnnn0b  9446  nn0le2is012  9562  btwnz  9599  uz11  9779  nn01to3  9851  zq  9860  xrltso  10031  xltnegi  10070  xnn0lenn0nn0  10100  xnn0xadd0  10102  iccleub  10166  fzdcel  10275  uznfz  10338  2ffzeq  10376  elfzonlteqm1  10456  icogelb  10526  flqeqceilz  10581  modqadd1  10624  modqmul1  10640  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  fzfig  10693  seqf1og  10784  m1expeven  10849  qsqeqor  10913  fundm2domnop0  11113  ccatrcl1  11195  pfxsuff1eqwrdeq  11284  wrdind  11307  wrd2ind  11308  swrdccat3blem  11324  caucvgrelemcau  11545  rexico  11786  fisumss  11958  fsum2dlemstep  12000  ntrivcvgap  12114  fprodssdc  12156  fprod2dlemstep  12188  0dvds  12377  alzdvds  12420  opoe  12461  omoe  12462  opeo  12463  omeo  12464  m1exp1  12467  nn0enne  12468  nn0o1gt2  12471  gcdneg  12558  dfgcd2  12590  algcvgblem  12626  algcvga  12628  eucalglt  12634  coprmdvds  12669  divgcdcoprmex  12679  cncongr1  12680  prm2orodd  12703  prm23lt5  12841  pockthi  12936  f1ocpbl  13399  f1ovscpbl  13400  f1olecpbl  13401  ismnddef  13506  lmodfopnelem1  14344  tg2  14790  tgcl  14794  neii1  14877  neii2  14879  txlm  15009  reopnap  15276  tgioo  15284  addcncntoplem  15291  gausslemma2dlem0i  15792  2lgslem2  15827  2lgs  15839  2lgsoddprmlem3  15846  uhgr0vb  15941  umgredg  16002  uspgrushgr  16037  uspgrupgr  16038  usgruspgr  16040  uhgr2edg  16063  edg0usgr  16104  egrsubgr  16120  0uhgrsubgr  16122  uhgrspansubgrlem  16133  vtxdg0v  16151  wlkpropg  16181  wlkv  16183  wlkvg  16185  wlkvtxeledgg  16201  wlkl1loop  16215  upgrwlkedg  16218  upgrwlkvtxedg  16221  uspgr2wlkeq  16222  wlkv0  16226  clwwlkccat  16258  clwwlknp  16274  clwwlkext2edg  16279  eupth2lem3lem4fi  16330  bj-elssuniab  16413  bj-nn0sucALT  16599  triap  16659