Theorem imbitrdi 250

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 215	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3imtr3g  295  3orel2  1480  exlimd  2203  cbvexdw  2327  ax13lem2  2367  cbvexd  2399  axc14  2454  mo3  2550  2eu3  2641  2eu6  2644  necon2bd  2948  necon2d  2955  necon4d  2956  spcimgft  3569  spc3egv  3585  elabgt  3654  reupick  4310  prneimg  4847  dfiun2g  5023  invdisj  5122  trin  5267  exexneq  5424  pwssun  5561  wefrc  5660  eqbrrdva  5859  elreldm  5924  elinxp  6009  xp11  6164  ssrnres  6167  suc11  6461  opelf  6742  dffo4  7094  onmindif2  7788  dftpos3  8224  frrlem13  8278  swoer  8728  domtriord  9118  nneneq  9204  nneneqOLD  9216  unblem1  9290  supnub  9452  infnlb  9482  en3lplem2  9603  suc11reg  9609  inf3lem2  9619  trcl  9718  tz9.13  9781  acndom  10041  carduniima  10086  cardinfima  10087  dfac5lem5  10117  fin23lem26  10315  hsmexlem2  10417  axcc4  10429  axdc3lem2  10441  axdclem2  10510  entric  10547  alephval2  10562  cfpwsdom  10574  fpwwe2lem8  10628  ltapr  11035  supsrlem  11101  sup2  12166  nnunb  12464  nneo  12642  indstr  12896  mul2lt0bi  13076  ngtmnft  13141  qsqueeze  13176  qextlt  13178  qextle  13179  icoshft  13446  injresinj  13749  swrdccatin2  14675  rexuzre  15295  rexico  15296  summo  15659  rpnnen2lem12  16164  divalglem5  16336  ndvdssub  16348  isprm7  16641  prmdvdsncoprmbd  16659  pc2dvds  16808  infpn2  16842  vdwnnlem3  16926  mreiincl  17536  intopsn  18574  pmtrrn2  19365  psgnunilem4  19402  ablfac1eulem  19979  lbsextlem3  20996  xrsdsreclb  21271  znleval  21410  elcls3  22897  isclo2  22902  tgcn  23066  cnprest  23103  ordthaus  23198  hauscmplem  23220  comppfsc  23346  kgencn2  23371  prdstopn  23442  xkohaus  23467  qtoptop2  23513  tgqtop  23526  filufint  23734  fclsbas  23835  alexsubALTlem3  23863  alexsubALTlem4  23864  ptcmplem2  23867  cldsubg  23925  isucn2  24094  metequiv2  24329  bcthlem5  25166  vieta1  26154  aannenlem2  26171  ulmbdd  26239  angpined  26666  rlimcnp2  26802  amgm  26827  ftalem3  26911  bposlem6  27126  nofv  27494  sltres  27499  nogt01o  27533  nosupprefixmo  27537  noinfprefixmo  27538  noetasuplem4  27573  uhgrvd00  29215  pthdlem2lem  29448  frcond2  29944  lnon0  30475  ocnel  30975  h1dn0  31229  cnlnssadj  31757  cvnbtwn2  31964  cvnbtwn3  31965  cvnbtwn4  31966  dmdbr2  31980  dmdbr3  31982  dmdbr4  31983  superpos  32031  atcvati  32063  mdsymlem4  32083  sumdmdii  32092  cdj3lem1  32111  elicoelioo  32413  archiabl  32771  bnj1280  34486  cusgr3cyclex  34582  loop1cycl  34583  erdszelem9  34645  satfvsucsuc  34811  untangtr  35144  dfon2lem6  35221  dfon2lem7  35222  outsideofrflx  35560  trer  35657  elicc3  35658  nn0prpw  35664  bj-syl66ib  35887  bj-cbvexdv  36134  bj-sblem1  36177  bj-spcimdv  36231  bj-spcimdvv  36232  topdifinffinlem  36684  icorempo  36688  isbasisrelowllem1  36692  relowlpssretop  36701  difunieq  36711  fvineqsneq  36749  wl-mo3t  36897  poimirlem23  36967  poimirlem29  36973  poimirlem32  36976  poimir  36977  mblfinlem2  36982  sdclem1  37067  fdc  37069  incsequz  37072  rngosn3  37248  0rngo  37351  dmncan1  37400  disjdmqscossss  38129  bicomdd  38180  prtlem15  38201  lsatcvat  38376  lfl1  38396  hlrelat2  38730  cvrat  38749  linepsubN  39079  2llnma3r  39115  dihjatcclem4  40748  dochexmidlem1  40787  sn-sup2  41797  rngunsnply  42370  onsupuni  42433  tfsconcatrn  42547  mptrcllem  42819  frege124d  42967  frege77  43146  frege116  43185  or3or  43229  clsk1indlem3  43249  ssralv2  43747  truniALT  43757  onfrALTlem3  43760  onfrALTlem2  43762  onfrALTlem1  43764  ax6e2ndeq  43775  stoweidlem62  45229  atbiffatnnb  46073  2reu3  46269  2reuimp  46274  gbowge7  46882  gbege6  46884  copisnmnd  46998  line2ylem  47591  line2xlem  47593  setrec1lem4  47889