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  1488  exlimd  2226  cbvexdw  2343  ax13lem2  2380  cbvexd  2412  axc14  2467  mo3  2564  2eu3  2654  2eu6  2657  necon2bd  2948  necon2d  2955  necon4d  2956  spcimgfi1OLD  3493  spc3egv  3545  elabgtOLD  3615  elabgtOLDOLD  3616  reupick  4269  prneimg  4797  dfiun2g  4972  invdisj  5071  trin  5204  exexneq  5387  pwssun  5523  wefrc  5625  eqbrrdva  5824  elreldm  5890  elinxp  5984  xp11  6139  ssrnres  6142  suc11  6432  opelf  6701  dffo4  7055  onmindif2  7761  dftpos3  8194  frrlem13  8248  swoer  8675  domtriord  9061  nneneq  9140  unblem1  9202  supnub  9375  infnlb  9406  en3lplem2  9534  suc11reg  9540  inf3lem2  9550  trcl  9649  tz9.13  9715  acndom  9973  carduniima  10018  cardinfima  10019  dfac5lem5  10049  fin23lem26  10247  hsmexlem2  10349  axcc4  10361  axdc3lem2  10373  axdclem2  10442  entric  10479  alephval2  10495  cfpwsdom  10507  fpwwe2lem8  10561  ltapr  10968  supsrlem  11034  sup2  12112  nnunb  12433  nneo  12613  indstr  12866  mul2lt0bi  13050  ngtmnft  13118  qsqueeze  13153  qextlt  13155  qextle  13156  icoshft  13426  injresinj  13746  swrdccatin2  14691  rexuzre  15315  rexico  15316  summo  15679  rpnnen2lem12  16192  divalglem5  16366  ndvdssub  16378  isprm7  16678  prmdvdsncoprmbd  16697  pc2dvds  16850  infpn2  16884  vdwnnlem3  16968  mreiincl  17558  intopsn  18622  pmtrrn2  19435  psgnunilem4  19472  ablfac1eulem  20049  lbsextlem3  21158  xrsdsreclb  21394  znleval  21534  elcls3  23048  isclo2  23053  tgcn  23217  cnprest  23254  ordthaus  23349  hauscmplem  23371  comppfsc  23497  kgencn2  23522  prdstopn  23593  xkohaus  23618  qtoptop2  23664  tgqtop  23677  filufint  23885  fclsbas  23986  alexsubALTlem3  24014  alexsubALTlem4  24015  ptcmplem2  24018  cldsubg  24076  isucn2  24243  metequiv2  24475  bcthlem5  25295  vieta1  26278  aannenlem2  26295  ulmbdd  26363  angpined  26794  rlimcnp2  26930  amgm  26954  ftalem3  27038  bposlem6  27252  nofv  27621  ltsres  27626  nogt01o  27660  nosupprefixmo  27664  noinfprefixmo  27665  noetasuplem4  27700  z12zsodd  28474  uhgrvd00  29603  pthdlem2lem  29835  frcond2  30337  lnon0  30869  ocnel  31369  h1dn0  31623  cnlnssadj  32151  cvnbtwn2  32358  cvnbtwn3  32359  cvnbtwn4  32360  dmdbr2  32374  dmdbr3  32376  dmdbr4  32377  superpos  32425  atcvati  32457  mdsymlem4  32477  sumdmdii  32486  cdj3lem1  32505  elicoelioo  32851  archiabl  33259  elrgspnlem4  33306  bnj1280  35162  rankval4b  35243  rankfilimbi  35244  tz9.1regs  35278  cusgr3cyclex  35318  loop1cycl  35319  erdszelem9  35381  satfvsucsuc  35547  untangtr  35896  dfon2lem6  35968  dfon2lem7  35969  outsideofrflx  36309  trer  36498  elicc3  36499  nn0prpw  36505  bj-syl66ib  36819  bj-cbvexdv  37107  bj-sblem1  37149  bj-spcimdv  37202  bj-spcimdvv  37203  bj-axseprep  37381  topdifinffinlem  37663  icorempo  37667  isbasisrelowllem1  37671  relowlpssretop  37680  difunieq  37690  fvineqsneq  37728  wl-mo3t  37901  poimirlem23  37964  poimirlem29  37970  poimirlem32  37973  poimir  37974  mblfinlem2  37979  sdclem1  38064  fdc  38066  incsequz  38069  rngosn3  38245  0rngo  38348  dmncan1  38397  sucmapleftuniq  38811  preuniqval  38817  disjdmqscossss  39227  bicomdd  39300  prtlem15  39321  lsatcvat  39496  lfl1  39516  hlrelat2  39849  cvrat  39868  linepsubN  40198  2llnma3r  40234  dihjatcclem4  41867  dochexmidlem1  41906  sn-sup2  42936  rngunsnply  43597  onsupuni  43657  tfsconcatrn  43770  mptrcllem  44040  frege124d  44188  frege77  44367  frege116  44406  or3or  44450  clsk1indlem3  44470  ssralv2  44958  truniALT  44968  onfrALTlem3  44971  onfrALTlem2  44973  onfrALTlem1  44975  ax6e2ndeq  44986  stoweidlem62  46490  atbiffatnnb  47360  2reu3  47558  2reuimp  47563  gbowge7  48239  gbege6  48241  copisnmnd  48645  line2ylem  49227  line2xlem  49229  setrec1lem4  50165