Theorem imbitrdi 252

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  3imtr3g  296  3orel2OLD  1493  exlimd  2230  cbvexdw  2347  ax13lem2  2384  cbvexd  2416  axc14  2471  mo3  2568  2eu3  2658  2eu6  2661  necon2bd  2951  necon2d  2958  necon4d  2959  spcimgfi1OLD  3496  spc3egv  3548  elabgtOLD  3618  reupick  4264  prneimg  4792  dfiun2g  4966  invdisj  5065  trin  5198  exexneq  5381  pwssun  5517  wefrc  5619  eqbrrdva  5818  elreldm  5884  elinxp  5978  xp11  6133  ssrnres  6136  suc11  6426  opelf  6695  dffo4  7051  onmindif2  7757  dftpos3  8191  frrlem13  8245  swoer  8672  domtriord  9058  nneneq  9137  unblem1  9199  supnub  9372  infnlb  9403  en3lplem2  9532  suc11reg  9538  inf3lem2  9548  trcl  9647  tz9.13  9713  acndom  9971  carduniima  10016  cardinfima  10017  dfac5lem5  10047  fin23lem26  10245  hsmexlem2  10347  axcc4  10359  axdc3lem2  10371  axdclem2  10440  entric  10477  alephval2  10493  cfpwsdom  10505  fpwwe2lem8  10559  ltapr  10966  supsrlem  11032  sup2  12110  nnunb  12431  nneo  12611  indstr  12864  mul2lt0bi  13048  ngtmnft  13116  qsqueeze  13151  qextlt  13153  qextle  13154  icoshft  13424  injresinj  13744  swrdccatin2  14689  rexuzre  15313  rexico  15314  summo  15677  rpnnen2lem12  16190  divalglem5  16364  ndvdssub  16376  isprm7  16676  prmdvdsncoprmbd  16695  pc2dvds  16848  infpn2  16882  vdwnnlem3  16966  mreiincl  17556  intopsn  18620  pmtrrn2  19433  psgnunilem4  19470  ablfac1eulem  20047  lbsextlem3  21160  xrsdsreclb  21396  znleval  21536  elcls3  23073  isclo2  23078  tgcn  23242  cnprest  23279  ordthaus  23374  hauscmplem  23396  comppfsc  23522  kgencn2  23547  prdstopn  23618  xkohaus  23643  qtoptop2  23689  tgqtop  23702  filufint  23910  fclsbas  24011  alexsubALTlem3  24039  alexsubALTlem4  24040  ptcmplem2  24043  cldsubg  24101  isucn2  24268  metequiv2  24500  bcthlem5  25320  vieta1  26303  aannenlem2  26320  ulmbdd  26388  angpined  26819  rlimcnp2  26955  amgm  26979  ftalem3  27063  bposlem6  27277  nofv  27646  ltsres  27651  nogt01o  27685  nosupprefixmo  27689  noinfprefixmo  27690  noetasuplem4  27725  z12zsodd  28499  uhgrvd00  29628  pthdlem2lem  29860  frcond2  30362  lnon0  30894  ocnel  31394  h1dn0  31648  cnlnssadj  32176  cvnbtwn2  32383  cvnbtwn3  32384  cvnbtwn4  32385  dmdbr2  32399  dmdbr3  32401  dmdbr4  32402  superpos  32450  atcvati  32482  mdsymlem4  32502  sumdmdii  32511  cdj3lem1  32530  elicoelioo  32877  archiabl  33286  elrgspnlem4  33333  bnj1280  35209  rankval4b  35288  rankfilimbi  35289  tz9.1regs  35322  cusgr3cyclex  35371  loop1cycl  35372  erdszelem9  35434  satfvsucsuc  35600  untangtr  35949  dfon2lem6  36021  dfon2lem7  36022  outsideofrflx  36362  trer  36551  elicc3  36552  nn0prpw  36558  bj-syl66ib  36872  bj-cbvexdv  37160  bj-sblem1  37202  bj-spcimdv  37255  bj-spcimdvv  37256  bj-axseprep  37434  topdifinffinlem  37716  icorempo  37720  isbasisrelowllem1  37724  relowlpssretop  37733  difunieq  37743  fvineqsneq  37781  wl-mo3t  37954  poimirlem23  38017  poimirlem29  38023  poimirlem32  38026  poimir  38027  mblfinlem2  38032  sdclem1  38117  fdc  38119  incsequz  38122  rngosn3  38298  0rngo  38401  dmncan1  38450  sucmapleftuniq  38864  preuniqval  38870  disjdmqscossss  39280  bicomdd  39353  prtlem15  39374  lsatcvat  39549  lfl1  39569  hlrelat2  39902  cvrat  39921  linepsubN  40251  2llnma3r  40287  dihjatcclem4  41920  dochexmidlem1  41959  sn-sup2  42988  rngunsnply  43621  onsupuni  43681  tfsconcatrn  43794  mptrcllem  44064  frege124d  44212  frege77  44391  frege116  44430  or3or  44474  clsk1indlem3  44494  ssralv2  44982  truniALT  44992  onfrALTlem3  44995  onfrALTlem2  44997  onfrALTlem1  44999  ax6e2ndeq  45010  stoweidlem62  46512  atbiffatnnb  47382  2reu3  47580  2reuimp  47585  gbowge7  48261  gbege6  48263  copisnmnd  48667  line2ylem  49249  line2xlem  49251  setrec1lem4  50187