Theorem imbitrdi 253

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3imtr3g  297  3orel2OLD  1505  exlimd  2252  cbvexdw  2369  ax13lem2  2406  cbvexd  2438  axc14  2493  mo3  2590  2eu3  2679  2eu6  2682  necon2bd  2972  necon2d  2979  necon4d  2980  spcimgfi1OLD  3515  spc3egv  3562  elabgtOLD  3632  reupick  4281  prneimg  4811  dfiun2g  4986  invdisj  5085  trin  5218  exexneq  5401  pwssun  5537  wefrc  5639  eqbrrdva  5839  elreldm  5909  elinxp  6003  xp11  6157  ssrnres  6160  suc11  6451  opelf  6721  dffo4  7080  onmindif2  7786  dftpos3  8219  frrlem13  8274  swoer  8705  domtriord  9091  nneneq  9170  unblem1  9232  supnub  9405  infnlb  9436  en3lplem2  9565  suc11reg  9571  inf3lem2  9581  trcl  9680  tz9.13  9746  acndom  10004  carduniima  10049  cardinfima  10050  dfac5lem5  10080  fin23lem26  10279  hsmexlem2  10381  axcc4  10393  axdc3lem2  10405  axdclem2  10474  entric  10511  alephval2  10527  cfpwsdom  10539  fpwwe2lem8  10593  ltapr  11000  supsrlem  11066  sup2  12145  nnunb  12474  nneo  12654  indstr  12914  mul2lt0bi  13098  ngtmnft  13166  qsqueeze  13201  qextlt  13203  qextle  13204  icoshft  13474  injresinj  13794  swrdccatin2  14739  rexuzre  15363  rexico  15364  summo  15727  rpnnen2lem12  16240  divalglem5  16414  ndvdssub  16426  isprm7  16726  prmdvdsncoprmbd  16745  pc2dvds  16898  infpn2  16932  vdwnnlem3  17016  mreiincl  17607  intopsn  18671  pmtrrn2  19483  psgnunilem4  19520  ablfac1eulem  20097  lbsextlem3  21210  xrsdsreclb  21446  znleval  21586  elcls3  23123  isclo2  23128  tgcn  23292  cnprest  23329  ordthaus  23424  hauscmplem  23446  comppfsc  23572  kgencn2  23597  prdstopn  23668  xkohaus  23693  qtoptop2  23739  tgqtop  23752  filufint  23960  fclsbas  24061  alexsubALTlem3  24089  alexsubALTlem4  24090  ptcmplem2  24093  cldsubg  24151  isucn2  24318  metequiv2  24550  bcthlem5  25370  vieta1  26353  aannenlem2  26370  ulmbdd  26438  angpined  26872  rlimcnp2  27008  amgm  27032  ftalem3  27116  bposlem6  27330  nofv  27698  ltsres  27703  nogt01o  27737  nosupprefixmo  27741  noinfprefixmo  27742  noetasuplem4  27777  z12zsodd  28552  uhgrvd00  29681  pthdlem2lem  29913  frcond2  30415  lnon0  30947  ocnel  31447  h1dn0  31701  cnlnssadj  32229  cvnbtwn2  32436  cvnbtwn3  32437  cvnbtwn4  32438  dmdbr2  32452  dmdbr3  32454  dmdbr4  32455  superpos  32503  atcvati  32535  mdsymlem4  32555  sumdmdii  32564  cdj3lem1  32583  elicoelioo  32930  archiabl  33339  elrgspnlem4  33387  bnj1280  35279  rankval4b  35360  rankfilimbi  35361  tz9.1regs  35394  onvfowev  35423  cusgr3cyclex  35450  loop1cycl  35451  erdszelem9  35513  satfvsucsuc  35679  untangtr  36028  dfon2lem6  36100  dfon2lem7  36101  outsideofrflx  36441  trer  36640  elicc3  36641  nn0prpw  36647  bj-syl66ib  36961  bj-cbvexdv  37249  bj-sblem1  37291  bj-spcimdv  37344  bj-spcimdvv  37345  bj-axseprep  37523  topdifinffinlem  37805  icorempo  37809  isbasisrelowllem1  37813  relowlpssretop  37822  difunieq  37832  fvineqsneq  37870  wl-mo3t  38043  poimirlem23  38106  poimirlem29  38112  poimirlem32  38115  poimir  38116  mblfinlem2  38121  sdclem1  38206  fdc  38208  incsequz  38211  rngosn3  38387  0rngo  38490  dmncan1  38539  sucmapleftuniq  38953  preuniqval  38959  disjdmqscossss  39369  bicomdd  39442  prtlem15  39463  lsatcvat  39638  lfl1  39658  hlrelat2  39991  cvrat  40010  linepsubN  40340  2llnma3r  40376  dihjatcclem4  42009  dochexmidlem1  42048  sn-sup2  43077  rngunsnply  43710  onsupuni  43770  tfsconcatrn  43883  mptrcllem  44153  frege124d  44301  frege77  44480  frege116  44519  or3or  44563  clsk1indlem3  44583  ssralv2  45071  truniALT  45081  onfrALTlem3  45084  onfrALTlem2  45086  onfrALTlem1  45088  ax6e2ndeq  45099  stoweidlem62  46600  atbiffatnnb  47470  2reu3  47668  2reuimp  47673  gbowge7  48349  gbege6  48351  copisnmnd  48755  line2ylem  49337  line2xlem  49339  setrec1lem4  50275