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  3494  spc3egv  3546  elabgtOLD  3616  elabgtOLDOLD  3617  reupick  4270  prneimg  4798  dfiun2g  4973  invdisj  5072  trin  5204  exexneq  5382  pwssun  5516  wefrc  5618  eqbrrdva  5818  elreldm  5884  elinxp  5978  xp11  6133  ssrnres  6136  suc11  6426  opelf  6695  dffo4  7049  onmindif2  7754  dftpos3  8187  frrlem13  8241  swoer  8668  domtriord  9054  nneneq  9133  unblem1  9195  supnub  9368  infnlb  9399  en3lplem2  9525  suc11reg  9531  inf3lem2  9541  trcl  9640  tz9.13  9706  acndom  9964  carduniima  10009  cardinfima  10010  dfac5lem5  10040  fin23lem26  10238  hsmexlem2  10340  axcc4  10352  axdc3lem2  10364  axdclem2  10433  entric  10470  alephval2  10486  cfpwsdom  10498  fpwwe2lem8  10552  ltapr  10959  supsrlem  11025  sup2  12103  nnunb  12424  nneo  12604  indstr  12857  mul2lt0bi  13041  ngtmnft  13109  qsqueeze  13144  qextlt  13146  qextle  13147  icoshft  13417  injresinj  13737  swrdccatin2  14682  rexuzre  15306  rexico  15307  summo  15670  rpnnen2lem12  16183  divalglem5  16357  ndvdssub  16369  isprm7  16669  prmdvdsncoprmbd  16688  pc2dvds  16841  infpn2  16875  vdwnnlem3  16959  mreiincl  17549  intopsn  18613  pmtrrn2  19426  psgnunilem4  19463  ablfac1eulem  20040  lbsextlem3  21150  xrsdsreclb  21403  znleval  21544  elcls3  23058  isclo2  23063  tgcn  23227  cnprest  23264  ordthaus  23359  hauscmplem  23381  comppfsc  23507  kgencn2  23532  prdstopn  23603  xkohaus  23628  qtoptop2  23674  tgqtop  23687  filufint  23895  fclsbas  23996  alexsubALTlem3  24024  alexsubALTlem4  24025  ptcmplem2  24028  cldsubg  24086  isucn2  24253  metequiv2  24485  bcthlem5  25305  vieta1  26289  aannenlem2  26306  ulmbdd  26376  angpined  26807  rlimcnp2  26943  amgm  26968  ftalem3  27052  bposlem6  27266  nofv  27635  ltsres  27640  nogt01o  27674  nosupprefixmo  27678  noinfprefixmo  27679  noetasuplem4  27714  z12zsodd  28488  uhgrvd00  29618  pthdlem2lem  29850  frcond2  30352  lnon0  30884  ocnel  31384  h1dn0  31638  cnlnssadj  32166  cvnbtwn2  32373  cvnbtwn3  32374  cvnbtwn4  32375  dmdbr2  32389  dmdbr3  32391  dmdbr4  32392  superpos  32440  atcvati  32472  mdsymlem4  32492  sumdmdii  32501  cdj3lem1  32520  elicoelioo  32866  archiabl  33274  elrgspnlem4  33321  bnj1280  35178  rankval4b  35259  rankfilimbi  35260  tz9.1regs  35294  cusgr3cyclex  35334  loop1cycl  35335  erdszelem9  35397  satfvsucsuc  35563  untangtr  35912  dfon2lem6  35984  dfon2lem7  35985  outsideofrflx  36325  trer  36514  elicc3  36515  nn0prpw  36521  bj-syl66ib  36835  bj-cbvexdv  37123  bj-sblem1  37165  bj-spcimdv  37218  bj-spcimdvv  37219  bj-axseprep  37397  topdifinffinlem  37677  icorempo  37681  isbasisrelowllem1  37685  relowlpssretop  37694  difunieq  37704  fvineqsneq  37742  wl-mo3t  37915  poimirlem23  37978  poimirlem29  37984  poimirlem32  37987  poimir  37988  mblfinlem2  37993  sdclem1  38078  fdc  38080  incsequz  38083  rngosn3  38259  0rngo  38362  dmncan1  38411  sucmapleftuniq  38825  preuniqval  38831  disjdmqscossss  39241  bicomdd  39314  prtlem15  39335  lsatcvat  39510  lfl1  39530  hlrelat2  39863  cvrat  39882  linepsubN  40212  2llnma3r  40248  dihjatcclem4  41881  dochexmidlem1  41920  sn-sup2  42950  rngunsnply  43615  onsupuni  43675  tfsconcatrn  43788  mptrcllem  44058  frege124d  44206  frege77  44385  frege116  44424  or3or  44468  clsk1indlem3  44488  ssralv2  44976  truniALT  44986  onfrALTlem3  44989  onfrALTlem2  44991  onfrALTlem1  44993  ax6e2ndeq  45004  stoweidlem62  46508  atbiffatnnb  47372  2reu3  47570  2reuimp  47575  gbowge7  48251  gbege6  48253  copisnmnd  48657  line2ylem  49239  line2xlem  49241  setrec1lem4  50177