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  4469  elinsn  4671  tppreqb  4768  sotri2  6123  sotri3  6124  somincom  6128  fnun  6651  fvmpti  6990  ovigg  7563  ndmovg  7602  onint  7802  tfindsg  7870  findsg  7907  resf1ext2b  7945  zfrep6OLD  7965  poxp2  8153  extmptsuppeq  8198  tfrlem9  8386  tfr3  8400  omlimcl  8579  oneo  8582  nnneo  8657  pssnn  9177  onomeneq  9222  inficl  9410  frmin  9746  updjud  10008  dfac2b  10202  axdc2lem  10519  axextnd  10669  canthp1lem2  10731  gchinf  10735  inatsk  10856  indpi  10985  ltaddpr2  11113  reclem2pr  11126  supsrlem  11189  axrrecex  11241  zeo  12778  nn0ind-raph  12792  fzm1  13734  fzind2  13916  addmodlteq  14082  bcpasc  14458  pr2pwpr  14617  swrdnnn0nd  14799  pwdif  16030  oddnn02np1  16511  oddge22np1  16512  evennn02n  16513  evennn2n  16514  bitsfzo  16598  bezoutlem1  16705  algcvgblem  16745  coprmdvds1  16820  qredeq  16825  prmreclem2  17088  ramtcl2  17182  divsfval  17712  joinval  18542  meetval  18556  gsumval3  20114  pgpfac1lem3a  20285  fiinopn  23212  restntr  23493  lly1stc  23808  dgradd2  26580  dgrcolem2  26586  asinneg  27207  ftalem2  27394  ftalem4  27396  ftalem5  27397  bpos1lem  27602  zabsle1  27616  lgsqrmodndvds  27673  incistruhgr  29650  fusgrfis  29904  uhgrnbgr0nb  29928  cusgrrusgr  30155  wlkswwlksf1o  30461  isclwwlknx  30620  clwwlknwwlksnb  30639  clwlknf1oclwwlknlem1  30665  frgrwopreglem3  30908  frgrreg  30988  frgrregord013  30989  h1de2ctlem  32150  pjclem4a  32793  pj3lem1  32801  chrelat2i  32960  sumdmdii  33010  elim2if  33133  bnj1468  35469  bnj517  35508  acycgrislfgr  35896  axextdist  36541  funtransport  36776  mh-setindnd  37305  bj-19.21t0  37722  bj-projval  37889  areacirc  38611  rngoueqz  38854  isdmn3  38988  ax12fromc15  39942  lkrlspeqN  40208  hlrelat2  40440  ps-1  40514  dalem54  40763  cdleme42c  41509  dihmeetlem6  42346  oe0suclim  44263  sdomne0  44398  sdomne0d  44399  frege124d  44746  uneqsn  45010  iotavalb  45399  2reuimp  48154  afv2orxorb  48267  iccpartnel  48489  fargshiftf1  48492  nprmdvdsfacm1lem2  48675  gbowge7  48830  sbgoldbwt  48844  bgoldbtbndlem1  48872  uspgrsprf1  49214  isidom3  49411  inisegn0a  49915