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  3orel2  1484  exlimd  2219  cbvexdw  2345  ax13lem2  2384  cbvexd  2416  axc14  2471  mo3  2567  2eu3  2657  2eu6  2660  necon2bd  2962  necon2d  2969  necon4d  2970  spcimgfi1OLD  3560  spc3egv  3616  elabgt  3685  elabgtOLD  3686  reupick  4348  prneimg  4879  dfiun2g  5053  invdisj  5152  trin  5295  exexneq  5454  pwssun  5590  wefrc  5694  eqbrrdva  5894  elreldm  5960  elinxp  6048  xp11  6206  ssrnres  6209  suc11  6502  opelf  6782  dffo4  7137  onmindif2  7843  dftpos3  8285  frrlem13  8339  swoer  8794  domtriord  9189  nneneq  9272  nneneqOLD  9284  unblem1  9356  supnub  9531  infnlb  9561  en3lplem2  9682  suc11reg  9688  inf3lem2  9698  trcl  9797  tz9.13  9860  acndom  10120  carduniima  10165  cardinfima  10166  dfac5lem5  10196  fin23lem26  10394  hsmexlem2  10496  axcc4  10508  axdc3lem2  10520  axdclem2  10589  entric  10626  alephval2  10641  cfpwsdom  10653  fpwwe2lem8  10707  ltapr  11114  supsrlem  11180  sup2  12251  nnunb  12549  nneo  12727  indstr  12981  mul2lt0bi  13163  ngtmnft  13228  qsqueeze  13263  qextlt  13265  qextle  13266  icoshft  13533  injresinj  13838  swrdccatin2  14777  rexuzre  15401  rexico  15402  summo  15765  rpnnen2lem12  16273  divalglem5  16445  ndvdssub  16457  isprm7  16755  prmdvdsncoprmbd  16774  pc2dvds  16926  infpn2  16960  vdwnnlem3  17044  mreiincl  17654  intopsn  18692  pmtrrn2  19502  psgnunilem4  19539  ablfac1eulem  20116  lbsextlem3  21185  xrsdsreclb  21454  znleval  21596  elcls3  23112  isclo2  23117  tgcn  23281  cnprest  23318  ordthaus  23413  hauscmplem  23435  comppfsc  23561  kgencn2  23586  prdstopn  23657  xkohaus  23682  qtoptop2  23728  tgqtop  23741  filufint  23949  fclsbas  24050  alexsubALTlem3  24078  alexsubALTlem4  24079  ptcmplem2  24082  cldsubg  24140  isucn2  24309  metequiv2  24544  bcthlem5  25381  vieta1  26372  aannenlem2  26389  ulmbdd  26459  angpined  26891  rlimcnp2  27027  amgm  27052  ftalem3  27136  bposlem6  27351  nofv  27720  sltres  27725  nogt01o  27759  nosupprefixmo  27763  noinfprefixmo  27764  noetasuplem4  27799  uhgrvd00  29570  pthdlem2lem  29803  frcond2  30299  lnon0  30830  ocnel  31330  h1dn0  31584  cnlnssadj  32112  cvnbtwn2  32319  cvnbtwn3  32320  cvnbtwn4  32321  dmdbr2  32335  dmdbr3  32337  dmdbr4  32338  superpos  32386  atcvati  32418  mdsymlem4  32438  sumdmdii  32447  cdj3lem1  32466  elicoelioo  32783  archiabl  33178  bnj1280  34996  cusgr3cyclex  35104  loop1cycl  35105  erdszelem9  35167  satfvsucsuc  35333  untangtr  35676  dfon2lem6  35752  dfon2lem7  35753  outsideofrflx  36091  trer  36282  elicc3  36283  nn0prpw  36289  bj-syl66ib  36521  bj-cbvexdv  36766  bj-sblem1  36808  bj-spcimdv  36861  bj-spcimdvv  36862  topdifinffinlem  37313  icorempo  37317  isbasisrelowllem1  37321  relowlpssretop  37330  difunieq  37340  fvineqsneq  37378  wl-mo3t  37530  poimirlem23  37603  poimirlem29  37609  poimirlem32  37612  poimir  37613  mblfinlem2  37618  sdclem1  37703  fdc  37705  incsequz  37708  rngosn3  37884  0rngo  37987  dmncan1  38036  disjdmqscossss  38759  bicomdd  38810  prtlem15  38831  lsatcvat  39006  lfl1  39026  hlrelat2  39360  cvrat  39379  linepsubN  39709  2llnma3r  39745  dihjatcclem4  41378  dochexmidlem1  41417  sn-sup2  42447  rngunsnply  43130  onsupuni  43190  tfsconcatrn  43304  mptrcllem  43575  frege124d  43723  frege77  43902  frege116  43941  or3or  43985  clsk1indlem3  44005  ssralv2  44502  truniALT  44512  onfrALTlem3  44515  onfrALTlem2  44517  onfrALTlem1  44519  ax6e2ndeq  44530  stoweidlem62  45983  atbiffatnnb  46827  2reu3  47025  2reuimp  47030  gbowge7  47637  gbege6  47639  copisnmnd  47892  line2ylem  48485  line2xlem  48487  setrec1lem4  48782