Theorem imbitrdi 251

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 216	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3imtr3g  295  3orel2OLD  1487  exlimd  2223  cbvexdw  2341  ax13lem2  2378  cbvexd  2410  axc14  2465  mo3  2561  2eu3  2651  2eu6  2654  necon2bd  2945  necon2d  2952  necon4d  2953  spcimgfi1OLD  3502  spc3egv  3554  elabgtOLD  3624  elabgtOLDOLD  3625  reupick  4278  prneimg  4805  dfiun2g  4980  invdisj  5079  trin  5211  exexneq  5379  pwssun  5511  wefrc  5613  eqbrrdva  5813  elreldm  5879  elinxp  5972  xp11  6127  ssrnres  6130  suc11  6420  opelf  6689  dffo4  7042  onmindif2  7746  dftpos3  8180  frrlem13  8234  swoer  8659  domtriord  9043  nneneq  9122  unblem1  9183  supnub  9353  infnlb  9384  en3lplem2  9510  suc11reg  9516  inf3lem2  9526  trcl  9625  tz9.13  9691  acndom  9949  carduniima  9994  cardinfima  9995  dfac5lem5  10025  fin23lem26  10223  hsmexlem2  10325  axcc4  10337  axdc3lem2  10349  axdclem2  10418  entric  10455  alephval2  10470  cfpwsdom  10482  fpwwe2lem8  10536  ltapr  10943  supsrlem  11009  sup2  12085  nnunb  12384  nneo  12563  indstr  12816  mul2lt0bi  13000  ngtmnft  13067  qsqueeze  13102  qextlt  13104  qextle  13105  icoshft  13375  injresinj  13693  swrdccatin2  14638  rexuzre  15262  rexico  15263  summo  15626  rpnnen2lem12  16136  divalglem5  16310  ndvdssub  16322  isprm7  16621  prmdvdsncoprmbd  16640  pc2dvds  16793  infpn2  16827  vdwnnlem3  16911  mreiincl  17500  intopsn  18564  pmtrrn2  19374  psgnunilem4  19411  ablfac1eulem  19988  lbsextlem3  21099  xrsdsreclb  21352  znleval  21493  elcls3  22999  isclo2  23004  tgcn  23168  cnprest  23205  ordthaus  23300  hauscmplem  23322  comppfsc  23448  kgencn2  23473  prdstopn  23544  xkohaus  23569  qtoptop2  23615  tgqtop  23628  filufint  23836  fclsbas  23937  alexsubALTlem3  23965  alexsubALTlem4  23966  ptcmplem2  23969  cldsubg  24027  isucn2  24194  metequiv2  24426  bcthlem5  25256  vieta1  26248  aannenlem2  26265  ulmbdd  26335  angpined  26768  rlimcnp2  26904  amgm  26929  ftalem3  27013  bposlem6  27228  nofv  27597  sltres  27602  nogt01o  27636  nosupprefixmo  27640  noinfprefixmo  27641  noetasuplem4  27676  zs12zodd  28393  uhgrvd00  29515  pthdlem2lem  29747  frcond2  30249  lnon0  30780  ocnel  31280  h1dn0  31534  cnlnssadj  32062  cvnbtwn2  32269  cvnbtwn3  32270  cvnbtwn4  32271  dmdbr2  32285  dmdbr3  32287  dmdbr4  32288  superpos  32336  atcvati  32368  mdsymlem4  32388  sumdmdii  32397  cdj3lem1  32416  elicoelioo  32765  archiabl  33174  elrgspnlem4  33219  bnj1280  35053  rankval4b  35132  rankfilimbi  35133  tz9.1regs  35151  cusgr3cyclex  35201  loop1cycl  35202  erdszelem9  35264  satfvsucsuc  35430  untangtr  35779  dfon2lem6  35851  dfon2lem7  35852  outsideofrflx  36192  trer  36381  elicc3  36382  nn0prpw  36388  bj-syl66ib  36620  bj-cbvexdv  36865  bj-sblem1  36907  bj-spcimdv  36960  bj-spcimdvv  36961  topdifinffinlem  37412  icorempo  37416  isbasisrelowllem1  37420  relowlpssretop  37429  difunieq  37439  fvineqsneq  37477  wl-mo3t  37641  poimirlem23  37703  poimirlem29  37709  poimirlem32  37712  poimir  37713  mblfinlem2  37718  sdclem1  37803  fdc  37805  incsequz  37808  rngosn3  37984  0rngo  38087  dmncan1  38136  sucmapleftuniq  38522  preuniqval  38528  disjdmqscossss  38921  bicomdd  38973  prtlem15  38994  lsatcvat  39169  lfl1  39189  hlrelat2  39522  cvrat  39541  linepsubN  39871  2llnma3r  39907  dihjatcclem4  41540  dochexmidlem1  41579  sn-sup2  42609  rngunsnply  43286  onsupuni  43346  tfsconcatrn  43459  mptrcllem  43730  frege124d  43878  frege77  44057  frege116  44096  or3or  44140  clsk1indlem3  44160  ssralv2  44648  truniALT  44658  onfrALTlem3  44661  onfrALTlem2  44663  onfrALTlem1  44665  ax6e2ndeq  44676  stoweidlem62  46184  atbiffatnnb  47036  2reu3  47234  2reuimp  47239  gbowge7  47887  gbege6  47889  copisnmnd  48293  line2ylem  48876  line2xlem  48878  setrec1lem4  49815