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  2225  cbvexdw  2343  ax13lem2  2380  cbvexd  2412  axc14  2467  mo3  2564  2eu3  2654  2eu6  2657  necon2bd  2948  necon2d  2955  necon4d  2956  spcimgfi1OLD  3505  spc3egv  3557  elabgtOLD  3627  elabgtOLDOLD  3628  reupick  4281  prneimg  4810  dfiun2g  4985  invdisj  5084  trin  5216  exexneq  5384  pwssun  5516  wefrc  5618  eqbrrdva  5818  elreldm  5884  elinxp  5978  xp11  6133  ssrnres  6136  suc11  6426  opelf  6695  dffo4  7048  onmindif2  7752  dftpos3  8186  frrlem13  8240  swoer  8666  domtriord  9051  nneneq  9130  unblem1  9192  supnub  9365  infnlb  9396  en3lplem2  9522  suc11reg  9528  inf3lem2  9538  trcl  9637  tz9.13  9703  acndom  9961  carduniima  10006  cardinfima  10007  dfac5lem5  10037  fin23lem26  10235  hsmexlem2  10337  axcc4  10349  axdc3lem2  10361  axdclem2  10430  entric  10467  alephval2  10483  cfpwsdom  10495  fpwwe2lem8  10549  ltapr  10956  supsrlem  11022  sup2  12098  nnunb  12397  nneo  12576  indstr  12829  mul2lt0bi  13013  ngtmnft  13081  qsqueeze  13116  qextlt  13118  qextle  13119  icoshft  13389  injresinj  13707  swrdccatin2  14652  rexuzre  15276  rexico  15277  summo  15640  rpnnen2lem12  16150  divalglem5  16324  ndvdssub  16336  isprm7  16635  prmdvdsncoprmbd  16654  pc2dvds  16807  infpn2  16841  vdwnnlem3  16925  mreiincl  17515  intopsn  18579  pmtrrn2  19389  psgnunilem4  19426  ablfac1eulem  20003  lbsextlem3  21115  xrsdsreclb  21368  znleval  21509  elcls3  23027  isclo2  23032  tgcn  23196  cnprest  23233  ordthaus  23328  hauscmplem  23350  comppfsc  23476  kgencn2  23501  prdstopn  23572  xkohaus  23597  qtoptop2  23643  tgqtop  23656  filufint  23864  fclsbas  23965  alexsubALTlem3  23993  alexsubALTlem4  23994  ptcmplem2  23997  cldsubg  24055  isucn2  24222  metequiv2  24454  bcthlem5  25284  vieta1  26276  aannenlem2  26293  ulmbdd  26363  angpined  26796  rlimcnp2  26932  amgm  26957  ftalem3  27041  bposlem6  27256  nofv  27625  ltsres  27630  nogt01o  27664  nosupprefixmo  27668  noinfprefixmo  27669  noetasuplem4  27704  z12zsodd  28478  uhgrvd00  29608  pthdlem2lem  29840  frcond2  30342  lnon0  30873  ocnel  31373  h1dn0  31627  cnlnssadj  32155  cvnbtwn2  32362  cvnbtwn3  32363  cvnbtwn4  32364  dmdbr2  32378  dmdbr3  32380  dmdbr4  32381  superpos  32429  atcvati  32461  mdsymlem4  32481  sumdmdii  32490  cdj3lem1  32509  elicoelioo  32858  archiabl  33280  elrgspnlem4  33327  bnj1280  35176  rankval4b  35256  rankfilimbi  35257  tz9.1regs  35290  cusgr3cyclex  35330  loop1cycl  35331  erdszelem9  35393  satfvsucsuc  35559  untangtr  35908  dfon2lem6  35980  dfon2lem7  35981  outsideofrflx  36321  trer  36510  elicc3  36511  nn0prpw  36517  exeltr  36665  bj-syl66ib  36755  bj-cbvexdv  37001  bj-sblem1  37043  bj-spcimdv  37096  bj-spcimdvv  37097  topdifinffinlem  37548  icorempo  37552  isbasisrelowllem1  37556  relowlpssretop  37565  difunieq  37575  fvineqsneq  37613  wl-mo3t  37777  poimirlem23  37840  poimirlem29  37846  poimirlem32  37849  poimir  37850  mblfinlem2  37855  sdclem1  37940  fdc  37942  incsequz  37945  rngosn3  38121  0rngo  38224  dmncan1  38273  sucmapleftuniq  38659  preuniqval  38665  disjdmqscossss  39058  bicomdd  39110  prtlem15  39131  lsatcvat  39306  lfl1  39326  hlrelat2  39659  cvrat  39678  linepsubN  40008  2llnma3r  40044  dihjatcclem4  41677  dochexmidlem1  41716  sn-sup2  42742  rngunsnply  43407  onsupuni  43467  tfsconcatrn  43580  mptrcllem  43850  frege124d  43998  frege77  44177  frege116  44216  or3or  44260  clsk1indlem3  44280  ssralv2  44768  truniALT  44778  onfrALTlem3  44781  onfrALTlem2  44783  onfrALTlem1  44785  ax6e2ndeq  44796  stoweidlem62  46302  atbiffatnnb  47154  2reu3  47352  2reuimp  47357  gbowge7  48005  gbege6  48007  copisnmnd  48411  line2ylem  48993  line2xlem  48995  setrec1lem4  49931