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  1488  exlimd  2226  cbvexdw  2344  ax13lem2  2381  cbvexd  2413  axc14  2468  mo3  2565  2eu3  2655  2eu6  2658  necon2bd  2949  necon2d  2956  necon4d  2957  spcimgfi1OLD  3507  spc3egv  3559  elabgtOLD  3629  elabgtOLDOLD  3630  reupick  4283  prneimg  4812  dfiun2g  4987  invdisj  5086  trin  5218  exexneq  5391  pwssun  5524  wefrc  5626  eqbrrdva  5826  elreldm  5892  elinxp  5986  xp11  6141  ssrnres  6144  suc11  6434  opelf  6703  dffo4  7057  onmindif2  7762  dftpos3  8196  frrlem13  8250  swoer  8677  domtriord  9063  nneneq  9142  unblem1  9204  supnub  9377  infnlb  9408  en3lplem2  9534  suc11reg  9540  inf3lem2  9550  trcl  9649  tz9.13  9715  acndom  9973  carduniima  10018  cardinfima  10019  dfac5lem5  10049  fin23lem26  10247  hsmexlem2  10349  axcc4  10361  axdc3lem2  10373  axdclem2  10442  entric  10479  alephval2  10495  cfpwsdom  10507  fpwwe2lem8  10561  ltapr  10968  supsrlem  11034  sup2  12110  nnunb  12409  nneo  12588  indstr  12841  mul2lt0bi  13025  ngtmnft  13093  qsqueeze  13128  qextlt  13130  qextle  13131  icoshft  13401  injresinj  13719  swrdccatin2  14664  rexuzre  15288  rexico  15289  summo  15652  rpnnen2lem12  16162  divalglem5  16336  ndvdssub  16348  isprm7  16647  prmdvdsncoprmbd  16666  pc2dvds  16819  infpn2  16853  vdwnnlem3  16937  mreiincl  17527  intopsn  18591  pmtrrn2  19401  psgnunilem4  19438  ablfac1eulem  20015  lbsextlem3  21127  xrsdsreclb  21380  znleval  21521  elcls3  23039  isclo2  23044  tgcn  23208  cnprest  23245  ordthaus  23340  hauscmplem  23362  comppfsc  23488  kgencn2  23513  prdstopn  23584  xkohaus  23609  qtoptop2  23655  tgqtop  23668  filufint  23876  fclsbas  23977  alexsubALTlem3  24005  alexsubALTlem4  24006  ptcmplem2  24009  cldsubg  24067  isucn2  24234  metequiv2  24466  bcthlem5  25296  vieta1  26288  aannenlem2  26305  ulmbdd  26375  angpined  26808  rlimcnp2  26944  amgm  26969  ftalem3  27053  bposlem6  27268  nofv  27637  ltsres  27642  nogt01o  27676  nosupprefixmo  27680  noinfprefixmo  27681  noetasuplem4  27716  z12zsodd  28490  uhgrvd00  29620  pthdlem2lem  29852  frcond2  30354  lnon0  30885  ocnel  31385  h1dn0  31639  cnlnssadj  32167  cvnbtwn2  32374  cvnbtwn3  32375  cvnbtwn4  32376  dmdbr2  32390  dmdbr3  32392  dmdbr4  32393  superpos  32441  atcvati  32473  mdsymlem4  32493  sumdmdii  32502  cdj3lem1  32521  elicoelioo  32868  archiabl  33291  elrgspnlem4  33338  bnj1280  35195  rankval4b  35275  rankfilimbi  35276  tz9.1regs  35309  cusgr3cyclex  35349  loop1cycl  35350  erdszelem9  35412  satfvsucsuc  35578  untangtr  35927  dfon2lem6  35999  dfon2lem7  36000  outsideofrflx  36340  trer  36529  elicc3  36530  nn0prpw  36536  exeltr  36684  bj-syl66ib  36776  bj-cbvexdv  37042  bj-sblem1  37084  bj-spcimdv  37137  bj-spcimdvv  37138  bj-axseprep  37316  topdifinffinlem  37596  icorempo  37600  isbasisrelowllem1  37604  relowlpssretop  37613  difunieq  37623  fvineqsneq  37661  wl-mo3t  37825  poimirlem23  37888  poimirlem29  37894  poimirlem32  37897  poimir  37898  mblfinlem2  37903  sdclem1  37988  fdc  37990  incsequz  37993  rngosn3  38169  0rngo  38272  dmncan1  38321  sucmapleftuniq  38735  preuniqval  38741  disjdmqscossss  39151  bicomdd  39224  prtlem15  39245  lsatcvat  39420  lfl1  39440  hlrelat2  39773  cvrat  39792  linepsubN  40122  2llnma3r  40158  dihjatcclem4  41791  dochexmidlem1  41830  sn-sup2  42855  rngunsnply  43520  onsupuni  43580  tfsconcatrn  43693  mptrcllem  43963  frege124d  44111  frege77  44290  frege116  44329  or3or  44373  clsk1indlem3  44393  ssralv2  44881  truniALT  44891  onfrALTlem3  44894  onfrALTlem2  44896  onfrALTlem1  44898  ax6e2ndeq  44909  stoweidlem62  46414  atbiffatnnb  47266  2reu3  47464  2reuimp  47469  gbowge7  48117  gbege6  48119  copisnmnd  48523  line2ylem  49105  line2xlem  49107  setrec1lem4  50043