Theorem imbitrdi 254

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3imtr3g  298  3orel2OLD  1516  exlimd  2256  cbvexdw  2370  ax13lem2  2407  cbvexd  2439  axc14  2494  mo3  2591  2eu3  2680  2eu6  2683  necon2bd  2973  necon2d  2980  necon4d  2981  spc3egv  3560  elabgtOLD  3630  reupick  4278  prneimg  4817  dfiun2g  4992  invdisj  5093  trin  5228  exexneq  5414  pwssun  5551  wefrc  5653  eqbrrdva  5853  elreldm  5923  elinxp  6016  xp11  6172  ssrnres  6175  suc11  6471  opelf  6740  dffo4  7100  onmindif2  7810  dftpos3  8246  frrlem13  8301  swoer  8732  domtriord  9125  nneneq  9204  unblem1  9266  supnub  9436  infnlb  9467  en3lplem2  9596  suc11reg  9602  inf3lem2  9612  trcl  9711  tz9.13  9777  acndom  10058  carduniima  10103  cardinfima  10104  dfac5lem5  10134  fin23lem26  10331  hsmexlem2  10433  axcc4  10445  axdc3lem2  10457  axdclem2  10526  entric  10569  alephval2  10585  cfpwsdom  10597  fpwwe2lem8  10651  ltapr  11058  supsrlem  11124  sup2  12199  nnunb  12528  nneo  12709  indstr  12969  mul2lt0bi  13154  ngtmnft  13222  qsqueeze  13257  qextlt  13259  qextle  13260  icoshft  13530  injresinj  13851  swrdccatin2  14802  rexuzre  15444  rexico  15445  summo  15807  rpnnen2lem12  16319  divalglem5  16493  ndvdssub  16505  isprm7  16805  prmdvdsncoprmbd  16824  pc2dvds  16977  infpn2  17011  vdwnnlem3  17095  mreiincl  17686  intopsn  18752  pmtrrn2  19593  psgnunilem4  19630  ablfac1eulem  20207  lbsextlem3  21353  xrsdsreclb  21633  znleval  21773  elcls3  23314  isclo2  23319  tgcn  23483  cnprest  23520  ordthaus  23615  hauscmplem  23637  comppfsc  23764  kgencn2  23789  prdstopn  23860  xkohaus  23885  qtoptop2  23931  tgqtop  23944  filufint  24152  fclsbas  24253  alexsubALTlem3  24281  alexsubALTlem4  24282  ptcmplem2  24285  cldsubg  24343  isucn2  24510  metequiv2  24742  bcthlem5  25562  vieta1  26551  aannenlem2  26572  ulmbdd  26641  angpined  27075  rlimcnp2  27211  amgm  27235  ftalem3  27319  bposlem6  27533  nofv  27901  ltsres  27906  nogt01o  27940  nosupprefixmo  27944  noinfprefixmo  27945  noetasuplem4  27980  z12zsodd  28755  uhgrvd00  30002  pthdlem2lem  30240  loop1cycl  30631  frcond2  30755  lnon0  31287  ocnel  31787  h1dn0  32041  cnlnssadj  32569  cvnbtwn2  32776  cvnbtwn3  32777  cvnbtwn4  32778  dmdbr2  32792  dmdbr3  32794  dmdbr4  32795  superpos  32843  atcvati  32875  mdsymlem4  32895  sumdmdii  32904  cdj3lem1  32923  elicoelioo  33257  archiabl  33646  elrgspnlem4  33693  bnj1280  35537  rankval4b  35615  rankfilimbi  35617  tz9.1regs  35668  onvfowev  35721  cusgr3cyclex  35733  erdszelem9  35786  satfvsucsuc  35952  untangtr  36301  dfon2lem6  36373  dfon2lem7  36374  outsideofrflx  36715  trer  36943  elicc3  36944  nn0prpw  36950  bj-syl66ib  37263  bj-cbvexdv  37551  bj-sblem1  37593  bj-spcimdv  37646  bj-spcimdvv  37647  bj-axseprep  37827  topdifinffinlem  38109  icorempo  38113  isbasisrelowllem1  38117  relowlpssretop  38126  difunieq  38136  fvineqsneq  38174  wl-mo3t  38347  poimirlem23  38400  poimirlem29  38406  poimirlem32  38409  poimir  38410  mblfinlem2  38415  findcard4  38471  sdclem1  38501  fdc  38503  incsequz  38506  rngosn3  38682  0rngo  38785  dmncan1  38834  sucmapleftuniq  39246  preuniqval  39252  disjdmqscossss  39662  bicomdd  39735  prtlem15  39756  lsatcvat  39931  lfl1  39951  hlrelat2  40284  cvrat  40303  linepsubN  40633  2llnma3r  40669  dihjatcclem4  42302  dochexmidlem1  42341  sn-sup2  43387  rngunsnply  44018  onsupuni  44078  tfsconcatrn  44191  mptrcllem  44461  frege124d  44609  frege77  44788  frege116  44827  or3or  44871  clsk1indlem3  44891  ssralv2  45362  truniALT  45372  onfrALTlem3  45375  onfrALTlem2  45377  onfrALTlem1  45379  ax6e2ndeq  45390  stoweidlem62  46898  atbiffatnnb  47808  2reu3  48006  2reuimp  48011  gbowge7  48687  gbege6  48689  copisnmnd  49092  idomcanl  49270  line2ylem  49689  line2xlem  49691  setrec1lem4  50624