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  exlimd  2258  cbvexdw  2372  ax13lem2  2408  cbvexd  2440  axc14  2495  mo3  2592  2eu3  2681  2eu6  2684  necon2bd  2975  necon2d  2982  necon4d  2983  spc3egv  3561  elabgtOLD  3630  reupick  4277  prneimg  4812  dfiun2g  4991  invdisj  5092  trin  5228  exexneq  5408  pwssun  5548  wefrc  5650  eqbrrdva  5855  elreldm  5925  elinxp  6021  xp11  6180  ssrnres  6183  suc11  6493  opelf  6768  dffo4  7130  onmindif2  7848  dftpos3  8292  frrlem13  8347  swoer  8780  domtriord  9173  nneneq  9252  unblem1  9315  supnub  9484  infnlb  9515  en3lplem2  9644  suc11reg  9650  inf3lem2  9660  trcl  9759  tz9.13  9828  rankval4b  9910  rankfilimbi  9932  setrec1lem4  10001  acndom  10160  carduniima  10205  cardinfima  10206  dfac5lem5  10236  fin23lem26  10433  hsmexlem2  10535  axcc4  10547  axdc3lem2  10559  axdclem2  10628  entric  10671  alephval2  10687  cfpwsdom  10699  fpwwe2lem8  10753  ltapr  11160  supsrlem  11226  sup2  12303  nnunb  12632  nneo  12813  indstr  13073  mul2lt0bi  13258  ngtmnft  13326  qsqueeze  13361  qextlt  13363  qextle  13364  icoshft  13634  injresinj  13956  swrdccatin2  14909  rexuzre  15552  rexico  15553  summo  15915  rpnnen2lem12  16425  divalglem5  16599  ndvdssub  16611  isprm7  16916  prmdvdsncoprmbd  16935  pc2dvds  17089  infpn2  17123  vdwnnlem3  17207  mreiincl  17798  intopsn  18864  pmtrrn2  19707  psgnunilem4  19744  ablfac1eulem  20321  lbsextlem3  21471  xrsdsreclb  21753  znleval  21893  elcls3  23434  isclo2  23439  tgcn  23603  cnprest  23640  ordthaus  23735  hauscmplem  23757  comppfsc  23884  kgencn2  23909  prdstopn  23980  xkohaus  24005  qtoptop2  24051  tgqtop  24064  filufint  24272  fclsbas  24373  alexsubALTlem3  24401  alexsubALTlem4  24402  ptcmplem2  24405  cldsubg  24463  isucn2  24630  metequiv2  24862  bcthlem5  25682  vieta1  26668  aannenlem2  26689  ulmbdd  26758  angpined  27191  rlimcnp2  27327  amgm  27351  ftalem3  27435  bposlem6  27649  nofv  28047  ltsres  28052  nogt01o  28086  nosupprefixmo  28090  noinfprefixmo  28091  noetasuplem4  28126  z12zsodd  28901  uhgrvd00  30148  pthdlem2lem  30386  loop1cycl  30777  frcond2  30901  lnon0  31433  ocnel  31933  h1dn0  32187  cnlnssadj  32715  cvnbtwn2  32922  cvnbtwn3  32923  cvnbtwn4  32924  dmdbr2  32938  dmdbr3  32940  dmdbr4  32941  superpos  32989  atcvati  33021  mdsymlem4  33041  sumdmdii  33050  cdj3lem1  33069  elicoelioo  33443  archiabl  33835  elrgspnlem4  33882  bnj1280  35733  ordunmax  35805  erscottd  35856  tz9.1regs  35915  onvfowev  36063  cusgr3cyclex  36081  erdszelem9  36144  satfvsucsuc  36310  untangtr  36670  dfon2lem6  36741  dfon2lem7  36742  outsideofrflx  37083  trer  37295  elicc3  37296  nn0prpw  37302  bj-syl66ib  37615  bj-cbvexdv  37903  bj-sblem1  37945  bj-spcimdv  37998  bj-spcimdvv  37999  bj-axseprep  38194  topdifinffinlem  38475  icorempo  38479  isbasisrelowllem1  38483  relowlpssretop  38492  difunieq  38502  fvineqsneq  38540  wl-mo3t  38713  poimirlem23  38766  poimirlem29  38772  poimirlem32  38775  poimir  38776  mblfinlem2  38781  findcard4  38837  sdclem1  38880  fdc  38882  incsequz  38885  rngosn3  39061  0rngo  39164  dmncan1  39213  sucmapleftuniq  39625  preuniqval  39631  disjdmqscossss  40041  bicomdd  40114  prtlem15  40135  lsatcvat  40310  lfl1  40330  hlrelat2  40663  cvrat  40682  linepsubN  41012  2llnma3r  41048  dihjatcclem4  42681  dochexmidlem1  42720  sn-sup2  43759  rngunsnply  44374  onsupuni  44434  tfsconcatrn  44547  mptrcllem  44816  frege124d  44964  frege77  45143  frege116  45182  or3or  45226  clsk1indlem3  45246  ssralv2  45716  truniALT  45726  onfrALTlem3  45729  onfrALTlem2  45731  onfrALTlem1  45733  ax6e2ndeq  45744  cocanss2  46125  stoweidlem62  47287  atbiffatnnb  48197  2reu3  48396  2reuimp  48401  gbowge7  49076  gbege6  49078  copisnmnd  49481  idomcanl  49659  line2ylem  50078  line2xlem  50080