Theorem imbitrdi 250

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem imbitrdi

Step	Hyp	Ref	Expression
1		imbitrdi.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		imbitrdi.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	2	biimpi 215	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  3imtr3g  295  3orel2  1484  exlimd  2210  cbvexdw  2334  ax13lem2  2374  cbvexd  2406  axc14  2461  mo3  2557  2eu3  2648  2eu6  2651  necon2bd  2955  necon2d  2962  necon4d  2963  spcimgft  3577  spc3egv  3593  elabgt  3662  reupick  4318  prneimg  4855  dfiun2g  5033  invdisj  5132  trin  5277  exexneq  5434  pwssun  5571  wefrc  5670  eqbrrdva  5869  elreldm  5934  elinxp  6019  xp11  6174  ssrnres  6177  suc11  6471  opelf  6752  dffo4  7104  onmindif2  7799  dftpos3  8233  frrlem13  8287  swoer  8737  domtriord  9127  nneneq  9213  nneneqOLD  9225  unblem1  9299  supnub  9461  infnlb  9491  en3lplem2  9612  suc11reg  9618  inf3lem2  9628  trcl  9727  tz9.13  9790  acndom  10050  carduniima  10095  cardinfima  10096  dfac5lem5  10126  fin23lem26  10324  hsmexlem2  10426  axcc4  10438  axdc3lem2  10450  axdclem2  10519  entric  10556  alephval2  10571  cfpwsdom  10583  fpwwe2lem8  10637  ltapr  11044  supsrlem  11110  sup2  12175  nnunb  12473  nneo  12651  indstr  12905  mul2lt0bi  13085  ngtmnft  13150  qsqueeze  13185  qextlt  13187  qextle  13188  icoshft  13455  injresinj  13758  swrdccatin2  14684  rexuzre  15304  rexico  15305  summo  15668  rpnnen2lem12  16173  divalglem5  16345  ndvdssub  16357  isprm7  16650  prmdvdsncoprmbd  16668  pc2dvds  16817  infpn2  16851  vdwnnlem3  16935  mreiincl  17545  intopsn  18580  pmtrrn2  19370  psgnunilem4  19407  ablfac1eulem  19984  lbsextlem3  20919  xrsdsreclb  21193  znleval  21330  elcls3  22808  isclo2  22813  tgcn  22977  cnprest  23014  ordthaus  23109  hauscmplem  23131  comppfsc  23257  kgencn2  23282  prdstopn  23353  xkohaus  23378  qtoptop2  23424  tgqtop  23437  filufint  23645  fclsbas  23746  alexsubALTlem3  23774  alexsubALTlem4  23775  ptcmplem2  23778  cldsubg  23836  isucn2  24005  metequiv2  24240  bcthlem5  25077  vieta1  26062  aannenlem2  26079  ulmbdd  26147  angpined  26572  rlimcnp2  26708  amgm  26732  ftalem3  26816  bposlem6  27029  nofv  27397  sltres  27402  nogt01o  27436  nosupprefixmo  27440  noinfprefixmo  27441  noetasuplem4  27476  uhgrvd00  29059  pthdlem2lem  29292  frcond2  29788  lnon0  30319  ocnel  30819  h1dn0  31073  cnlnssadj  31601  cvnbtwn2  31808  cvnbtwn3  31809  cvnbtwn4  31810  dmdbr2  31824  dmdbr3  31826  dmdbr4  31827  superpos  31875  atcvati  31907  mdsymlem4  31927  sumdmdii  31936  cdj3lem1  31955  elicoelioo  32257  archiabl  32615  bnj1280  34330  cusgr3cyclex  34426  loop1cycl  34427  erdszelem9  34489  satfvsucsuc  34655  untangtr  34988  dfon2lem6  35065  dfon2lem7  35066  outsideofrflx  35404  trer  35505  elicc3  35506  nn0prpw  35512  bj-syl66ib  35735  bj-cbvexdv  35982  bj-sblem1  36025  bj-spcimdv  36079  bj-spcimdvv  36080  topdifinffinlem  36532  icorempo  36536  isbasisrelowllem1  36540  relowlpssretop  36549  difunieq  36559  fvineqsneq  36597  wl-mo3t  36745  poimirlem23  36815  poimirlem29  36821  poimirlem32  36824  poimir  36825  mblfinlem2  36830  sdclem1  36915  fdc  36917  incsequz  36920  rngosn3  37096  0rngo  37199  dmncan1  37248  disjdmqscossss  37977  bicomdd  38028  prtlem15  38049  lsatcvat  38224  lfl1  38244  hlrelat2  38578  cvrat  38597  linepsubN  38927  2llnma3r  38963  dihjatcclem4  40596  dochexmidlem1  40635  sn-sup2  41645  rngunsnply  42218  onsupuni  42281  tfsconcatrn  42395  mptrcllem  42667  frege124d  42815  frege77  42994  frege116  43033  or3or  43077  clsk1indlem3  43097  ssralv2  43595  truniALT  43605  onfrALTlem3  43608  onfrALTlem2  43610  onfrALTlem1  43612  ax6e2ndeq  43623  stoweidlem62  45077  atbiffatnnb  45921  2reu3  46117  2reuimp  46122  gbowge7  46730  gbege6  46732  copisnmnd  46846  line2ylem  47525  line2xlem  47527  setrec1lem4  47823