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  5833  elunirn  5906  oprabid  6049  op1steq  6341  f1o2ndf1  6392  reldmtpos  6418  rntpos  6422  nntri3or  6660  nnaordex  6695  nnawordex  6696  findcard2  7077  findcard2s  7078  mkvprop  7356  cc2lem  7484  lt2addnq  7623  lt2mulnq  7624  genpelvl  7731  genpelvu  7732  distrlem5prl  7805  distrlem5pru  7806  caucvgprlemnkj  7885  map2psrprg  8024  rereceu  8108  ltxrlt  8244  0mnnnnn0  9433  elnnnn0b  9445  nn0le2is012  9561  btwnz  9598  uz11  9778  nn01to3  9850  zq  9859  xrltso  10030  xltnegi  10069  xnn0lenn0nn0  10099  xnn0xadd0  10101  iccleub  10165  fzdcel  10274  uznfz  10337  2ffzeq  10375  elfzonlteqm1  10454  icogelb  10524  flqeqceilz  10579  modqadd1  10622  modqmul1  10638  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  fzfig  10691  seqf1og  10782  m1expeven  10847  qsqeqor  10911  fundm2domnop0  11108  ccatrcl1  11190  pfxsuff1eqwrdeq  11279  wrdind  11302  wrd2ind  11303  swrdccat3blem  11319  caucvgrelemcau  11540  rexico  11781  fisumss  11952  fsum2dlemstep  11994  ntrivcvgap  12108  fprodssdc  12150  fprod2dlemstep  12182  0dvds  12371  alzdvds  12414  opoe  12455  omoe  12456  opeo  12457  omeo  12458  m1exp1  12461  nn0enne  12462  nn0o1gt2  12465  gcdneg  12552  dfgcd2  12584  algcvgblem  12620  algcvga  12622  eucalglt  12628  coprmdvds  12663  divgcdcoprmex  12673  cncongr1  12674  prm2orodd  12697  prm23lt5  12835  pockthi  12930  f1ocpbl  13393  f1ovscpbl  13394  f1olecpbl  13395  ismnddef  13500  lmodfopnelem1  14337  tg2  14783  tgcl  14787  neii1  14870  neii2  14872  txlm  15002  reopnap  15269  tgioo  15277  addcncntoplem  15284  gausslemma2dlem0i  15785  2lgslem2  15820  2lgs  15832  2lgsoddprmlem3  15839  uhgr0vb  15934  umgredg  15995  uspgrushgr  16030  uspgrupgr  16031  usgruspgr  16033  uhgr2edg  16056  edg0usgr  16097  egrsubgr  16113  0uhgrsubgr  16115  uhgrspansubgrlem  16126  vtxdg0v  16144  wlkpropg  16174  wlkv  16176  wlkvg  16178  wlkvtxeledgg  16194  wlkl1loop  16208  upgrwlkedg  16211  upgrwlkvtxedg  16214  uspgr2wlkeq  16215  wlkv0  16219  clwwlkccat  16251  clwwlknp  16267  clwwlkext2edg  16272  bj-elssuniab  16387  bj-nn0sucALT  16573  triap  16633