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  2221  cbvexdw  2339  ax13lem2  2376  cbvexd  2408  axc14  2463  mo3  2559  2eu3  2649  2eu6  2652  necon2bd  2944  necon2d  2951  necon4d  2952  spcimgfi1OLD  3503  spc3egv  3558  elabgtOLD  3628  elabgtOLDOLD  3629  reupick  4279  prneimg  4806  dfiun2g  4980  invdisj  5077  trin  5209  exexneq  5377  pwssun  5508  wefrc  5610  eqbrrdva  5809  elreldm  5875  elinxp  5968  xp11  6122  ssrnres  6125  suc11  6415  opelf  6684  dffo4  7036  onmindif2  7740  dftpos3  8174  frrlem13  8228  swoer  8653  domtriord  9036  nneneq  9115  unblem1  9176  supnub  9346  infnlb  9377  en3lplem2  9503  suc11reg  9509  inf3lem2  9519  trcl  9618  tz9.13  9681  acndom  9939  carduniima  9984  cardinfima  9985  dfac5lem5  10015  fin23lem26  10213  hsmexlem2  10315  axcc4  10327  axdc3lem2  10339  axdclem2  10408  entric  10445  alephval2  10460  cfpwsdom  10472  fpwwe2lem8  10526  ltapr  10933  supsrlem  10999  sup2  12075  nnunb  12374  nneo  12554  indstr  12811  mul2lt0bi  12995  ngtmnft  13062  qsqueeze  13097  qextlt  13099  qextle  13100  icoshft  13370  injresinj  13688  swrdccatin2  14633  rexuzre  15257  rexico  15258  summo  15621  rpnnen2lem12  16131  divalglem5  16305  ndvdssub  16317  isprm7  16616  prmdvdsncoprmbd  16635  pc2dvds  16788  infpn2  16822  vdwnnlem3  16906  mreiincl  17495  intopsn  18559  pmtrrn2  19370  psgnunilem4  19407  ablfac1eulem  19984  lbsextlem3  21095  xrsdsreclb  21348  znleval  21489  elcls3  22996  isclo2  23001  tgcn  23165  cnprest  23202  ordthaus  23297  hauscmplem  23319  comppfsc  23445  kgencn2  23470  prdstopn  23541  xkohaus  23566  qtoptop2  23612  tgqtop  23625  filufint  23833  fclsbas  23934  alexsubALTlem3  23962  alexsubALTlem4  23963  ptcmplem2  23966  cldsubg  24024  isucn2  24191  metequiv2  24423  bcthlem5  25253  vieta1  26245  aannenlem2  26262  ulmbdd  26332  angpined  26765  rlimcnp2  26901  amgm  26926  ftalem3  27010  bposlem6  27225  nofv  27594  sltres  27599  nogt01o  27633  nosupprefixmo  27637  noinfprefixmo  27638  noetasuplem4  27673  zs12zodd  28390  uhgrvd00  29511  pthdlem2lem  29743  frcond2  30242  lnon0  30773  ocnel  31273  h1dn0  31527  cnlnssadj  32055  cvnbtwn2  32262  cvnbtwn3  32263  cvnbtwn4  32264  dmdbr2  32278  dmdbr3  32280  dmdbr4  32281  superpos  32329  atcvati  32361  mdsymlem4  32381  sumdmdii  32390  cdj3lem1  32409  elicoelioo  32756  archiabl  33162  elrgspnlem4  33207  bnj1280  35027  rankval4b  35104  rankfilimbi  35105  tz9.1regs  35118  cusgr3cyclex  35168  loop1cycl  35169  erdszelem9  35231  satfvsucsuc  35397  untangtr  35746  dfon2lem6  35821  dfon2lem7  35822  outsideofrflx  36160  trer  36349  elicc3  36350  nn0prpw  36356  bj-syl66ib  36588  bj-cbvexdv  36833  bj-sblem1  36875  bj-spcimdv  36928  bj-spcimdvv  36929  topdifinffinlem  37380  icorempo  37384  isbasisrelowllem1  37388  relowlpssretop  37397  difunieq  37407  fvineqsneq  37445  wl-mo3t  37609  poimirlem23  37682  poimirlem29  37688  poimirlem32  37691  poimir  37692  mblfinlem2  37697  sdclem1  37782  fdc  37784  incsequz  37787  rngosn3  37963  0rngo  38066  dmncan1  38115  disjdmqscossss  38840  bicomdd  38892  prtlem15  38913  lsatcvat  39088  lfl1  39108  hlrelat2  39441  cvrat  39460  linepsubN  39790  2llnma3r  39826  dihjatcclem4  41459  dochexmidlem1  41498  sn-sup2  42523  rngunsnply  43201  onsupuni  43261  tfsconcatrn  43374  mptrcllem  43645  frege124d  43793  frege77  43972  frege116  44011  or3or  44055  clsk1indlem3  44075  ssralv2  44563  truniALT  44573  onfrALTlem3  44576  onfrALTlem2  44578  onfrALTlem1  44580  ax6e2ndeq  44591  stoweidlem62  46099  atbiffatnnb  46942  2reu3  47140  2reuimp  47145  gbowge7  47793  gbege6  47795  copisnmnd  48199  line2ylem  48782  line2xlem  48784  setrec1lem4  49721