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  2374  cbvexd  2406  axc14  2461  mo3  2557  2eu3  2647  2eu6  2650  necon2bd  2941  necon2d  2948  necon4d  2949  spcimgfi1OLD  3505  spc3egv  3560  elabgtOLD  3630  elabgtOLDOLD  3631  reupick  4282  prneimg  4808  dfiun2g  4983  invdisj  5081  trin  5213  exexneq  5381  pwssun  5515  wefrc  5617  eqbrrdva  5816  elreldm  5881  elinxp  5974  xp11  6128  ssrnres  6131  suc11  6420  opelf  6689  dffo4  7041  onmindif2  7747  dftpos3  8184  frrlem13  8238  swoer  8663  domtriord  9047  nneneq  9130  unblem1  9197  supnub  9371  infnlb  9402  en3lplem2  9528  suc11reg  9534  inf3lem2  9544  trcl  9643  tz9.13  9706  acndom  9964  carduniima  10009  cardinfima  10010  dfac5lem5  10040  fin23lem26  10238  hsmexlem2  10340  axcc4  10352  axdc3lem2  10364  axdclem2  10433  entric  10470  alephval2  10485  cfpwsdom  10497  fpwwe2lem8  10551  ltapr  10958  supsrlem  11024  sup2  12099  nnunb  12398  nneo  12578  indstr  12835  mul2lt0bi  13019  ngtmnft  13086  qsqueeze  13121  qextlt  13123  qextle  13124  icoshft  13394  injresinj  13709  swrdccatin2  14653  rexuzre  15278  rexico  15279  summo  15642  rpnnen2lem12  16152  divalglem5  16326  ndvdssub  16338  isprm7  16637  prmdvdsncoprmbd  16656  pc2dvds  16809  infpn2  16843  vdwnnlem3  16927  mreiincl  17516  intopsn  18546  pmtrrn2  19357  psgnunilem4  19394  ablfac1eulem  19971  lbsextlem3  21085  xrsdsreclb  21338  znleval  21479  elcls3  22986  isclo2  22991  tgcn  23155  cnprest  23192  ordthaus  23287  hauscmplem  23309  comppfsc  23435  kgencn2  23460  prdstopn  23531  xkohaus  23556  qtoptop2  23602  tgqtop  23615  filufint  23823  fclsbas  23924  alexsubALTlem3  23952  alexsubALTlem4  23953  ptcmplem2  23956  cldsubg  24014  isucn2  24182  metequiv2  24414  bcthlem5  25244  vieta1  26236  aannenlem2  26253  ulmbdd  26323  angpined  26756  rlimcnp2  26892  amgm  26917  ftalem3  27001  bposlem6  27216  nofv  27585  sltres  27590  nogt01o  27624  nosupprefixmo  27628  noinfprefixmo  27629  noetasuplem4  27664  zs12zodd  28377  uhgrvd00  29498  pthdlem2lem  29730  frcond2  30229  lnon0  30760  ocnel  31260  h1dn0  31514  cnlnssadj  32042  cvnbtwn2  32249  cvnbtwn3  32250  cvnbtwn4  32251  dmdbr2  32265  dmdbr3  32267  dmdbr4  32268  superpos  32316  atcvati  32348  mdsymlem4  32368  sumdmdii  32377  cdj3lem1  32396  elicoelioo  32734  archiabl  33150  elrgspnlem4  33195  bnj1280  34986  tz9.1regs  35066  cusgr3cyclex  35108  loop1cycl  35109  erdszelem9  35171  satfvsucsuc  35337  untangtr  35686  dfon2lem6  35761  dfon2lem7  35762  outsideofrflx  36100  trer  36289  elicc3  36290  nn0prpw  36296  bj-syl66ib  36528  bj-cbvexdv  36773  bj-sblem1  36815  bj-spcimdv  36868  bj-spcimdvv  36869  topdifinffinlem  37320  icorempo  37324  isbasisrelowllem1  37328  relowlpssretop  37337  difunieq  37347  fvineqsneq  37385  wl-mo3t  37549  poimirlem23  37622  poimirlem29  37628  poimirlem32  37631  poimir  37632  mblfinlem2  37637  sdclem1  37722  fdc  37724  incsequz  37727  rngosn3  37903  0rngo  38006  dmncan1  38055  disjdmqscossss  38780  bicomdd  38832  prtlem15  38853  lsatcvat  39028  lfl1  39048  hlrelat2  39382  cvrat  39401  linepsubN  39731  2llnma3r  39767  dihjatcclem4  41400  dochexmidlem1  41439  sn-sup2  42464  rngunsnply  43142  onsupuni  43202  tfsconcatrn  43315  mptrcllem  43586  frege124d  43734  frege77  43913  frege116  43952  or3or  43996  clsk1indlem3  44016  ssralv2  44505  truniALT  44515  onfrALTlem3  44518  onfrALTlem2  44520  onfrALTlem1  44522  ax6e2ndeq  44533  stoweidlem62  46044  atbiffatnnb  46897  2reu3  47095  2reuimp  47100  gbowge7  47748  gbege6  47750  copisnmnd  48154  line2ylem  48737  line2xlem  48739  setrec1lem4  49676