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  1679  ax11i  1762  equveli  1807  eupickbi  2162  nfabdw  2394  rgen2a  2587  reu6  2996  sseq0  3538  disjel  3551  preq12b  3858  prel12  3859  prneimg  3862  elinti  3942  exmidundif  4302  opthreg  4660  elreldm  4964  issref  5126  relcnvtr  5263  relresfld  5273  funopg  5367  funimass2  5415  f0dom0  5539  fvimacnv  5771  funopdmsn  5842  elunirn  5917  oprabid  6060  op1steq  6351  f1o2ndf1  6402  fvn0elsuppb  6430  suppfnss  6435  reldmtpos  6462  rntpos  6466  nntri3or  6704  nnaordex  6739  nnawordex  6740  findcard2  7121  findcard2s  7122  mkvprop  7400  cc2lem  7528  lt2addnq  7667  lt2mulnq  7668  genpelvl  7775  genpelvu  7776  distrlem5prl  7849  distrlem5pru  7850  caucvgprlemnkj  7929  map2psrprg  8068  rereceu  8152  ltxrlt  8287  0mnnnnn0  9476  elnnnn0b  9488  nn0le2is012  9606  btwnz  9643  uz11  9823  nn01to3  9895  zq  9904  xrltso  10075  xltnegi  10114  xnn0lenn0nn0  10144  xnn0xadd0  10146  iccleub  10210  fzdcel  10320  uznfz  10383  2ffzeq  10421  elfzonlteqm1  10501  icogelb  10571  flqeqceilz  10626  modqadd1  10669  modqmul1  10685  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  fzfig  10738  seqf1og  10829  m1expeven  10894  qsqeqor  10958  fundm2domnop0  11158  ccatrcl1  11240  pfxsuff1eqwrdeq  11329  wrdind  11352  wrd2ind  11353  swrdccat3blem  11369  caucvgrelemcau  11603  rexico  11844  fisumss  12016  fsum2dlemstep  12058  ntrivcvgap  12172  fprodssdc  12214  fprod2dlemstep  12246  0dvds  12435  alzdvds  12478  opoe  12519  omoe  12520  opeo  12521  omeo  12522  m1exp1  12525  nn0enne  12526  nn0o1gt2  12529  gcdneg  12616  dfgcd2  12648  algcvgblem  12684  algcvga  12686  eucalglt  12692  coprmdvds  12727  divgcdcoprmex  12737  cncongr1  12738  prm2orodd  12761  prm23lt5  12899  pockthi  12994  f1ocpbl  13457  f1ovscpbl  13458  f1olecpbl  13459  ismnddef  13564  lmodfopnelem1  14403  tg2  14854  tgcl  14858  neii1  14941  neii2  14943  txlm  15073  reopnap  15340  tgioo  15348  addcncntoplem  15355  gausslemma2dlem0i  15859  2lgslem2  15894  2lgs  15906  2lgsoddprmlem3  15913  uhgr0vb  16008  umgredg  16069  uspgrushgr  16104  uspgrupgr  16105  usgruspgr  16107  uhgr2edg  16130  edg0usgr  16171  egrsubgr  16187  0uhgrsubgr  16189  uhgrspansubgrlem  16200  vtxdg0v  16218  wlkpropg  16248  wlkv  16250  wlkvg  16252  wlkvtxeledgg  16268  wlkl1loop  16282  upgrwlkedg  16285  upgrwlkvtxedg  16288  uspgr2wlkeq  16289  wlkv0  16293  clwwlkccat  16325  clwwlknp  16341  clwwlkext2edg  16346  eupth2lem3lem4fi  16397  bj-elssuniab  16492  bj-nn0sucALT  16677  triap  16744