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  3506  spc3egv  3558  elabgtOLD  3628  elabgtOLDOLD  3629  reupick  4282  prneimg  4811  dfiun2g  4986  invdisj  5085  trin  5217  exexneq  5385  pwssun  5517  wefrc  5619  eqbrrdva  5819  elreldm  5885  elinxp  5979  xp11  6134  ssrnres  6137  suc11  6427  opelf  6696  dffo4  7050  onmindif2  7754  dftpos3  8188  frrlem13  8242  swoer  8669  domtriord  9055  nneneq  9134  unblem1  9196  supnub  9369  infnlb  9400  en3lplem2  9526  suc11reg  9532  inf3lem2  9542  trcl  9641  tz9.13  9707  acndom  9965  carduniima  10010  cardinfima  10011  dfac5lem5  10041  fin23lem26  10239  hsmexlem2  10341  axcc4  10353  axdc3lem2  10365  axdclem2  10434  entric  10471  alephval2  10487  cfpwsdom  10499  fpwwe2lem8  10553  ltapr  10960  supsrlem  11026  sup2  12102  nnunb  12401  nneo  12580  indstr  12833  mul2lt0bi  13017  ngtmnft  13085  qsqueeze  13120  qextlt  13122  qextle  13123  icoshft  13393  injresinj  13711  swrdccatin2  14656  rexuzre  15280  rexico  15281  summo  15644  rpnnen2lem12  16154  divalglem5  16328  ndvdssub  16340  isprm7  16639  prmdvdsncoprmbd  16658  pc2dvds  16811  infpn2  16845  vdwnnlem3  16929  mreiincl  17519  intopsn  18583  pmtrrn2  19393  psgnunilem4  19430  ablfac1eulem  20007  lbsextlem3  21119  xrsdsreclb  21372  znleval  21513  elcls3  23031  isclo2  23036  tgcn  23200  cnprest  23237  ordthaus  23332  hauscmplem  23354  comppfsc  23480  kgencn2  23505  prdstopn  23576  xkohaus  23601  qtoptop2  23647  tgqtop  23660  filufint  23868  fclsbas  23969  alexsubALTlem3  23997  alexsubALTlem4  23998  ptcmplem2  24001  cldsubg  24059  isucn2  24226  metequiv2  24458  bcthlem5  25288  vieta1  26280  aannenlem2  26297  ulmbdd  26367  angpined  26800  rlimcnp2  26936  amgm  26961  ftalem3  27045  bposlem6  27260  nofv  27629  sltres  27634  nogt01o  27668  nosupprefixmo  27672  noinfprefixmo  27673  noetasuplem4  27708  zs12zodd  28461  uhgrvd00  29591  pthdlem2lem  29823  frcond2  30325  lnon0  30856  ocnel  31356  h1dn0  31610  cnlnssadj  32138  cvnbtwn2  32345  cvnbtwn3  32346  cvnbtwn4  32347  dmdbr2  32361  dmdbr3  32363  dmdbr4  32364  superpos  32412  atcvati  32444  mdsymlem4  32464  sumdmdii  32473  cdj3lem1  32492  elicoelioo  32839  archiabl  33261  elrgspnlem4  33308  bnj1280  35157  rankval4b  35237  rankfilimbi  35238  tz9.1regs  35271  cusgr3cyclex  35311  loop1cycl  35312  erdszelem9  35374  satfvsucsuc  35540  untangtr  35889  dfon2lem6  35961  dfon2lem7  35962  outsideofrflx  36302  trer  36491  elicc3  36492  nn0prpw  36498  bj-syl66ib  36730  bj-cbvexdv  36976  bj-sblem1  37018  bj-spcimdv  37071  bj-spcimdvv  37072  topdifinffinlem  37523  icorempo  37527  isbasisrelowllem1  37531  relowlpssretop  37540  difunieq  37550  fvineqsneq  37588  wl-mo3t  37752  poimirlem23  37815  poimirlem29  37821  poimirlem32  37824  poimir  37825  mblfinlem2  37830  sdclem1  37915  fdc  37917  incsequz  37920  rngosn3  38096  0rngo  38199  dmncan1  38248  sucmapleftuniq  38662  preuniqval  38668  disjdmqscossss  39078  bicomdd  39151  prtlem15  39172  lsatcvat  39347  lfl1  39367  hlrelat2  39700  cvrat  39719  linepsubN  40049  2llnma3r  40085  dihjatcclem4  41718  dochexmidlem1  41757  sn-sup2  42782  rngunsnply  43447  onsupuni  43507  tfsconcatrn  43620  mptrcllem  43890  frege124d  44038  frege77  44217  frege116  44256  or3or  44300  clsk1indlem3  44320  ssralv2  44808  truniALT  44818  onfrALTlem3  44821  onfrALTlem2  44823  onfrALTlem1  44825  ax6e2ndeq  44836  stoweidlem62  46342  atbiffatnnb  47194  2reu3  47392  2reuimp  47397  gbowge7  48045  gbege6  48047  copisnmnd  48451  line2ylem  49033  line2xlem  49035  setrec1lem4  49971