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  2219  cbvexdw  2337  ax13lem2  2374  cbvexd  2406  axc14  2461  mo3  2557  2eu3  2647  2eu6  2650  necon2bd  2941  necon2d  2948  necon4d  2949  spcimgfi1OLD  3514  spc3egv  3569  elabgtOLD  3639  elabgtOLDOLD  3640  reupick  4292  prneimg  4818  dfiun2g  4994  invdisj  5093  trin  5226  exexneq  5394  pwssun  5530  wefrc  5632  eqbrrdva  5833  elreldm  5899  elinxp  5990  xp11  6148  ssrnres  6151  suc11  6441  opelf  6721  dffo4  7075  onmindif2  7783  dftpos3  8223  frrlem13  8277  swoer  8702  domtriord  9087  nneneq  9170  unblem1  9239  supnub  9413  infnlb  9444  en3lplem2  9566  suc11reg  9572  inf3lem2  9582  trcl  9681  tz9.13  9744  acndom  10004  carduniima  10049  cardinfima  10050  dfac5lem5  10080  fin23lem26  10278  hsmexlem2  10380  axcc4  10392  axdc3lem2  10404  axdclem2  10473  entric  10510  alephval2  10525  cfpwsdom  10537  fpwwe2lem8  10591  ltapr  10998  supsrlem  11064  sup2  12139  nnunb  12438  nneo  12618  indstr  12875  mul2lt0bi  13059  ngtmnft  13126  qsqueeze  13161  qextlt  13163  qextle  13164  icoshft  13434  injresinj  13749  swrdccatin2  14694  rexuzre  15319  rexico  15320  summo  15683  rpnnen2lem12  16193  divalglem5  16367  ndvdssub  16379  isprm7  16678  prmdvdsncoprmbd  16697  pc2dvds  16850  infpn2  16884  vdwnnlem3  16968  mreiincl  17557  intopsn  18581  pmtrrn2  19390  psgnunilem4  19427  ablfac1eulem  20004  lbsextlem3  21070  xrsdsreclb  21330  znleval  21464  elcls3  22970  isclo2  22975  tgcn  23139  cnprest  23176  ordthaus  23271  hauscmplem  23293  comppfsc  23419  kgencn2  23444  prdstopn  23515  xkohaus  23540  qtoptop2  23586  tgqtop  23599  filufint  23807  fclsbas  23908  alexsubALTlem3  23936  alexsubALTlem4  23937  ptcmplem2  23940  cldsubg  23998  isucn2  24166  metequiv2  24398  bcthlem5  25228  vieta1  26220  aannenlem2  26237  ulmbdd  26307  angpined  26740  rlimcnp2  26876  amgm  26901  ftalem3  26985  bposlem6  27200  nofv  27569  sltres  27574  nogt01o  27608  nosupprefixmo  27612  noinfprefixmo  27613  noetasuplem4  27648  uhgrvd00  29462  pthdlem2lem  29697  frcond2  30196  lnon0  30727  ocnel  31227  h1dn0  31481  cnlnssadj  32009  cvnbtwn2  32216  cvnbtwn3  32217  cvnbtwn4  32218  dmdbr2  32232  dmdbr3  32234  dmdbr4  32235  superpos  32283  atcvati  32315  mdsymlem4  32335  sumdmdii  32344  cdj3lem1  32363  elicoelioo  32701  archiabl  33152  elrgspnlem4  33196  bnj1280  35010  cusgr3cyclex  35123  loop1cycl  35124  erdszelem9  35186  satfvsucsuc  35352  untangtr  35701  dfon2lem6  35776  dfon2lem7  35777  outsideofrflx  36115  trer  36304  elicc3  36305  nn0prpw  36311  bj-syl66ib  36543  bj-cbvexdv  36788  bj-sblem1  36830  bj-spcimdv  36883  bj-spcimdvv  36884  topdifinffinlem  37335  icorempo  37339  isbasisrelowllem1  37343  relowlpssretop  37352  difunieq  37362  fvineqsneq  37400  wl-mo3t  37564  poimirlem23  37637  poimirlem29  37643  poimirlem32  37646  poimir  37647  mblfinlem2  37652  sdclem1  37737  fdc  37739  incsequz  37742  rngosn3  37918  0rngo  38021  dmncan1  38070  disjdmqscossss  38795  bicomdd  38847  prtlem15  38868  lsatcvat  39043  lfl1  39063  hlrelat2  39397  cvrat  39416  linepsubN  39746  2llnma3r  39782  dihjatcclem4  41415  dochexmidlem1  41454  sn-sup2  42479  rngunsnply  43158  onsupuni  43218  tfsconcatrn  43331  mptrcllem  43602  frege124d  43750  frege77  43929  frege116  43968  or3or  44012  clsk1indlem3  44032  ssralv2  44521  truniALT  44531  onfrALTlem3  44534  onfrALTlem2  44536  onfrALTlem1  44538  ax6e2ndeq  44549  stoweidlem62  46060  atbiffatnnb  46913  2reu3  47111  2reuimp  47116  gbowge7  47764  gbege6  47766  copisnmnd  48157  line2ylem  48740  line2xlem  48742  setrec1lem4  49679