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  294  3orel2  1485  exlimd  2211  cbvexdw  2335  ax13lem2  2375  cbvexd  2407  axc14  2462  mo3  2558  2eu3  2649  2eu6  2652  necon2bd  2956  necon2d  2963  necon4d  2964  spcimgft  3577  spc3egv  3593  elabgt  3661  reupick  4317  prneimg  4854  dfiun2g  5032  invdisj  5131  trin  5276  exexneq  5433  pwssun  5570  wefrc  5669  eqbrrdva  5867  elreldm  5932  elinxp  6017  xp11  6171  ssrnres  6174  suc11  6468  opelf  6749  dffo4  7101  onmindif2  7791  dftpos3  8225  frrlem13  8279  swoer  8729  domtriord  9119  nneneq  9205  nneneqOLD  9217  unblem1  9291  supnub  9453  infnlb  9483  en3lplem2  9604  suc11reg  9610  inf3lem2  9620  trcl  9719  tz9.13  9782  acndom  10042  carduniima  10087  cardinfima  10088  dfac5lem5  10118  fin23lem26  10316  hsmexlem2  10418  axcc4  10430  axdc3lem2  10442  axdclem2  10511  entric  10548  alephval2  10563  cfpwsdom  10575  fpwwe2lem8  10629  ltapr  11036  supsrlem  11102  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  18569  pmtrrn2  19322  psgnunilem4  19359  ablfac1eulem  19936  lbsextlem3  20765  xrsdsreclb  20984  znleval  21101  elcls3  22578  isclo2  22583  tgcn  22747  cnprest  22784  ordthaus  22879  hauscmplem  22901  comppfsc  23027  kgencn2  23052  prdstopn  23123  xkohaus  23148  qtoptop2  23194  tgqtop  23207  filufint  23415  fclsbas  23516  alexsubALTlem3  23544  alexsubALTlem4  23545  ptcmplem2  23548  cldsubg  23606  isucn2  23775  metequiv2  24010  bcthlem5  24836  vieta1  25816  aannenlem2  25833  ulmbdd  25901  angpined  26324  rlimcnp2  26460  amgm  26484  ftalem3  26568  bposlem6  26781  nofv  27149  sltres  27154  nogt01o  27188  nosupprefixmo  27192  noinfprefixmo  27193  noetasuplem4  27228  uhgrvd00  28780  pthdlem2lem  29013  frcond2  29509  lnon0  30038  ocnel  30538  h1dn0  30792  cnlnssadj  31320  cvnbtwn2  31527  cvnbtwn3  31528  cvnbtwn4  31529  dmdbr2  31543  dmdbr3  31545  dmdbr4  31546  superpos  31594  atcvati  31626  mdsymlem4  31646  sumdmdii  31655  cdj3lem1  31674  elicoelioo  31976  archiabl  32331  bnj1280  34019  cusgr3cyclex  34115  loop1cycl  34116  erdszelem9  34178  satfvsucsuc  34344  untangtr  34671  dfon2lem6  34748  dfon2lem7  34749  outsideofrflx  35087  trer  35189  elicc3  35190  nn0prpw  35196  bj-syl66ib  35419  bj-cbvexdv  35666  bj-sblem1  35709  bj-spcimdv  35763  bj-spcimdvv  35764  topdifinffinlem  36216  icorempo  36220  isbasisrelowllem1  36224  relowlpssretop  36233  difunieq  36243  fvineqsneq  36281  wl-mo3t  36429  poimirlem23  36499  poimirlem29  36505  poimirlem32  36508  poimir  36509  mblfinlem2  36514  sdclem1  36599  fdc  36601  incsequz  36604  rngosn3  36780  0rngo  36883  dmncan1  36932  disjdmqscossss  37661  bicomdd  37712  prtlem15  37733  lsatcvat  37908  lfl1  37928  hlrelat2  38262  cvrat  38281  linepsubN  38611  2llnma3r  38647  dihjatcclem4  40280  dochexmidlem1  40319  sn-sup2  41338  rngunsnply  41900  onsupuni  41963  tfsconcatrn  42077  mptrcllem  42349  frege124d  42497  frege77  42676  frege116  42715  or3or  42759  clsk1indlem3  42779  ssralv2  43277  truniALT  43287  onfrALTlem3  43290  onfrALTlem2  43292  onfrALTlem1  43294  ax6e2ndeq  43305  stoweidlem62  44764  atbiffatnnb  45608  2reu3  45804  2reuimp  45809  gbowge7  46417  gbege6  46419  copisnmnd  46565  line2ylem  47390  line2xlem  47392  setrec1lem4  47688