Theorem biimtrrdi 257

Description: A mixed syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

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

Assertion

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

Proof of Theorem biimtrrdi

Step	Hyp	Ref	Expression
1		biimtrrdi.1	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
2	1	biimprd 251	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 36	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  ralnralall  4472  elinsn  4672  tppreqb  4770  sotri2  6141  sotri3  6142  somincom  6146  fnun  6683  fvmpti  7023  ovigg  7597  ndmovg  7636  onint  7838  tfindsg  7906  findsg  7943  resf1ext2b  7981  zfrep6OLD  8001  poxp2  8197  extmptsuppeq  8243  tfrlem9  8431  tfr3  8445  omlimcl  8624  oneo  8627  nnneo  8702  pssnn  9222  onomeneq  9267  inficl  9454  frmin  9790  updjud  10052  dfac2b  10248  axdc2lem  10565  axextnd  10715  canthp1lem2  10777  gchinf  10781  inatsk  10902  indpi  11031  ltaddpr2  11159  reclem2pr  11172  supsrlem  11235  axrrecex  11287  zeo  12825  nn0ind-raph  12839  fzm1  13781  fzind2  13963  addmodlteq  14129  bcpasc  14506  pr2pwpr  14665  swrdnnn0nd  14848  pwdif  16081  oddnn02np1  16562  oddge22np1  16563  evennn02n  16564  evennn2n  16565  bitsfzo  16649  bezoutlem1  16756  algcvgblem  16796  coprmdvds1  16871  qredeq  16876  prmreclem2  17139  ramtcl2  17233  divsfval  17769  joinval  18599  meetval  18613  gsumval3  20172  pgpfac1lem3a  20343  fiinopn  23274  restntr  23555  lly1stc  23870  dgradd2  26642  dgrcolem2  26648  asinneg  27271  ftalem2  27458  ftalem4  27460  ftalem5  27461  bpos1lem  27666  zabsle1  27680  lgsqrmodndvds  27737  incistruhgr  29714  fusgrfis  29968  uhgrnbgr0nb  29992  cusgrrusgr  30219  wlkswwlksf1o  30525  isclwwlknx  30684  clwwlknwwlksnb  30703  clwlknf1oclwwlknlem1  30729  frgrwopreglem3  30972  frgrreg  31052  frgrregord013  31053  h1de2ctlem  32214  pjclem4a  32857  pj3lem1  32865  chrelat2i  33024  sumdmdii  33074  elim2if  33238  bnj1468  35587  bnj517  35626  acycgrislfgr  36115  axextdist  36776  funtransport  37011  mh-setindnd  37540  bj-19.21t0  37957  bj-projval  38124  areacirc  38899  rngoueqz  39140  isdmn3  39274  ax12fromc15  40228  lkrlspeqN  40494  hlrelat2  40726  ps-1  40800  dalem54  41049  cdleme42c  41795  dihmeetlem6  42632  oe0suclim  44540  sdomne0  44675  sdomne0d  44676  frege124d  45022  uneqsn  45286  iotavalb  45674  2reuimp  48459  afv2orxorb  48571  iccpartnel  48793  fargshiftf1  48796  nprmdvdsfacm1lem2  48979  gbowge7  49134  sbgoldbwt  49148  bgoldbtbndlem1  49176  uspgrsprf1  49518  isidom3  49773  inisegn0a  50278