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  2375  cbvexd  2407  axc14  2462  mo3  2558  2eu3  2648  2eu6  2651  necon2bd  2942  necon2d  2949  necon4d  2950  spcimgfi1OLD  3517  spc3egv  3572  elabgtOLD  3642  elabgtOLDOLD  3643  reupick  4295  prneimg  4821  dfiun2g  4997  invdisj  5096  trin  5229  exexneq  5397  pwssun  5533  wefrc  5635  eqbrrdva  5836  elreldm  5902  elinxp  5993  xp11  6151  ssrnres  6154  suc11  6444  opelf  6724  dffo4  7078  onmindif2  7786  dftpos3  8226  frrlem13  8280  swoer  8705  domtriord  9093  nneneq  9176  unblem1  9246  supnub  9420  infnlb  9451  en3lplem2  9573  suc11reg  9579  inf3lem2  9589  trcl  9688  tz9.13  9751  acndom  10011  carduniima  10056  cardinfima  10057  dfac5lem5  10087  fin23lem26  10285  hsmexlem2  10387  axcc4  10399  axdc3lem2  10411  axdclem2  10480  entric  10517  alephval2  10532  cfpwsdom  10544  fpwwe2lem8  10598  ltapr  11005  supsrlem  11071  sup2  12146  nnunb  12445  nneo  12625  indstr  12882  mul2lt0bi  13066  ngtmnft  13133  qsqueeze  13168  qextlt  13170  qextle  13171  icoshft  13441  injresinj  13756  swrdccatin2  14701  rexuzre  15326  rexico  15327  summo  15690  rpnnen2lem12  16200  divalglem5  16374  ndvdssub  16386  isprm7  16685  prmdvdsncoprmbd  16704  pc2dvds  16857  infpn2  16891  vdwnnlem3  16975  mreiincl  17564  intopsn  18588  pmtrrn2  19397  psgnunilem4  19434  ablfac1eulem  20011  lbsextlem3  21077  xrsdsreclb  21337  znleval  21471  elcls3  22977  isclo2  22982  tgcn  23146  cnprest  23183  ordthaus  23278  hauscmplem  23300  comppfsc  23426  kgencn2  23451  prdstopn  23522  xkohaus  23547  qtoptop2  23593  tgqtop  23606  filufint  23814  fclsbas  23915  alexsubALTlem3  23943  alexsubALTlem4  23944  ptcmplem2  23947  cldsubg  24005  isucn2  24173  metequiv2  24405  bcthlem5  25235  vieta1  26227  aannenlem2  26244  ulmbdd  26314  angpined  26747  rlimcnp2  26883  amgm  26908  ftalem3  26992  bposlem6  27207  nofv  27576  sltres  27581  nogt01o  27615  nosupprefixmo  27619  noinfprefixmo  27620  noetasuplem4  27655  uhgrvd00  29469  pthdlem2lem  29704  frcond2  30203  lnon0  30734  ocnel  31234  h1dn0  31488  cnlnssadj  32016  cvnbtwn2  32223  cvnbtwn3  32224  cvnbtwn4  32225  dmdbr2  32239  dmdbr3  32241  dmdbr4  32242  superpos  32290  atcvati  32322  mdsymlem4  32342  sumdmdii  32351  cdj3lem1  32370  elicoelioo  32708  archiabl  33159  elrgspnlem4  33203  bnj1280  35017  cusgr3cyclex  35130  loop1cycl  35131  erdszelem9  35193  satfvsucsuc  35359  untangtr  35708  dfon2lem6  35783  dfon2lem7  35784  outsideofrflx  36122  trer  36311  elicc3  36312  nn0prpw  36318  bj-syl66ib  36550  bj-cbvexdv  36795  bj-sblem1  36837  bj-spcimdv  36890  bj-spcimdvv  36891  topdifinffinlem  37342  icorempo  37346  isbasisrelowllem1  37350  relowlpssretop  37359  difunieq  37369  fvineqsneq  37407  wl-mo3t  37571  poimirlem23  37644  poimirlem29  37650  poimirlem32  37653  poimir  37654  mblfinlem2  37659  sdclem1  37744  fdc  37746  incsequz  37749  rngosn3  37925  0rngo  38028  dmncan1  38077  disjdmqscossss  38802  bicomdd  38854  prtlem15  38875  lsatcvat  39050  lfl1  39070  hlrelat2  39404  cvrat  39423  linepsubN  39753  2llnma3r  39789  dihjatcclem4  41422  dochexmidlem1  41461  sn-sup2  42486  rngunsnply  43165  onsupuni  43225  tfsconcatrn  43338  mptrcllem  43609  frege124d  43757  frege77  43936  frege116  43975  or3or  44019  clsk1indlem3  44039  ssralv2  44528  truniALT  44538  onfrALTlem3  44541  onfrALTlem2  44543  onfrALTlem1  44545  ax6e2ndeq  44556  stoweidlem62  46067  atbiffatnnb  46917  2reu3  47115  2reuimp  47120  gbowge7  47768  gbege6  47770  copisnmnd  48161  line2ylem  48744  line2xlem  48746  setrec1lem4  49683